proposition: Lemma fun_eta_5 : forall A1 A2 A3 A4 A5 B (f : A1 -> A2 -> A3 -> A4 -> A5 -> B), (fun x1 x2 x3 x4 x5 => f x1 x2 x3 x4 x5) = f.
proof: Proof. Proof using. intros. apply~ fun_ext_4. Qed.
imports: TLC(LibTactics LibAxioms)