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

State before:
n : ℕ
F : TypeFun n
⊢ reverseArgs (reverseArgs F) = F
Tactic:
unfold reverseArgs
State after:
n : ℕ
F : TypeFun n
⊢ (fun α => F (Vec.reverse (Vec.reverse α))) = F

State before:
n : ℕ
F : TypeFun n
⊢ (fun α => F (Vec.reverse (Vec.reverse α))) = F
Tactic:
simp only [Vec.reverse_involution]
State after:
no goals