proposition: Lemma ABS_prod_mk_pair (A B : Type') (x : A) (y : B) : ABS_prod (mk_pair x y) = (x,y).
proof: Proof. unfold ABS_prod. match goal with [|- ε ?x = _] => set (Q := x); set (q := ε Q) end. rewrite (surjective_pairing q). assert (i : exists q, Q q). exists (x,y). reflexivity. generalize (ε_spec i); fold q; unfold Q; intro h. apply mk_pair_inj in h. destruct h as [h1 h2]. rewrite h1, h2. reflexivity. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts