proposition: Lemma mk_pair_inj (A B : Type') (x x' : A) (y y' : B) : mk_pair x y = mk_pair x' y' -> x = x' /\ y = y'.
proof: Proof. intro e; generalize (ext_fun e); clear e; intro e. generalize (ext_fun (e x)); clear e; intro e. generalize (e y); clear e. unfold mk_pair. rewrite refl_is_True, refl_is_True, True_and_True, sym, is_True. intro h; exact h. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts