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

State before:
n : ℕ
F : CurriedTypeFun n
⊢ curried (ofCurried F) = F
Tactic:
simp only [curried, ofCurried, reverseArgs_involution]
State after:
n : ℕ
F : CurriedTypeFun n
⊢ curriedAux (ofCurriedAux F) = F

State before:
n : ℕ
F : CurriedTypeFun n
⊢ curriedAux (ofCurriedAux F) = F
Tactic:
apply curriedAux_ofCurriedAux_involution
State after:
no goals