Theorem: TypeFun.ofCurried_curried_involution (Qpf/Util/TypeFun.lean)

State before:
n : ℕ
F : TypeFun n
⊢ ofCurried (curried F) = F
Tactic:
simp only [ofCurried, curried, ofCurriedAux_curriedAux_involution]
State after:
n : ℕ
F : TypeFun n
⊢ reverseArgs (reverseArgs F) = F

State before:
n : ℕ
F : TypeFun n
⊢ reverseArgs (reverseArgs F) = F
Tactic:
apply reverseArgs_involution
State after:
no goals