proposition: Lemma lem1 : forall f x : E, axioms f -> inc x f -> x = pair (pr1 x) (V (pr1 x) f).
proof: Proof. ir. unfold axioms in H. xd. set (z := pr1 x) in *. assert (ex (fun y : E => inc (pair z y) f)). apply ex_intro with (pr2 x). unfold z in |- *. rewrite H. am. am. set (K := choose_pr H2) in *. assert (inc (pair z (V z f)) f). am. ap H1. am. am. rewrite pr1_pair. tv. Qed.
imports: set_theory