proposition: Lemma pred_ext_1 : forall (P Q : forall (x1:A1), Prop), (forall x1, P x1 <-> Q x1) -> P = Q.
proof: Proof. Proof using. repeat (intros; apply fun_ext_dep). intros. apply~ prop_ext. Qed.
imports: TLC(LibTactics LibAxioms)