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