proposition: Lemma axiom_5 : forall {A B : Type'} (r : A -> B -> Prop), ((fun x : A -> B -> Prop => exists a : A, exists b : B, x = (@mk_pair A B a b)) r) = ((@REP_prod A B (@ABS_prod A B r)) = r).
proof: Proof. intros A B f. simpl. apply prop_ext. intros [a [b e]]. subst. rewrite ABS_prod_mk_pair. reflexivity. generalize (ABS_prod f); intros [a b] e. subst. exists a. exists b. reflexivity. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts