proposition: Lemma fun_ext_4 : forall (f g: forall (x1:A1) (x2:A2 x1) (x3:A3 x2) (x4:A4 x3), A5 x4), (forall x1 x2 x3 x4, f x1 x2 x3 x4 = g x1 x2 x3 x4) -> f = g.
proof: Proof. Proof using. repeat (intros; apply fun_ext_dep). auto. Qed.
imports: TLC(LibTactics LibAxioms)