proposition: Lemma INJ_INVERSE2 {A B C : Type'} : forall P : A -> B -> C, (forall x1 : A, forall y1 : B, forall x2 : A, forall y2 : B, ((P x1 y1) = (P x2 y2)) = ((x1 = x2) /\ (y1 = y2))) -> exists X : C -> A, exists Y : C -> B, forall x : A, forall y : B, ((X (P x y)) = x) /\ ((Y (P x y)) = y).
proof: Proof. intros f h. exists (fun c => ε (fun a => exists b, f a b = c)). exists (fun c => ε (fun b => exists a, f a b = c)). intros a b. split. match goal with [|- ε ?x = _] => set (Q := x); set (q := ε Q) end. assert (i : exists a, Q a). exists a. exists b. reflexivity. generalize (ε_spec i). fold q. unfold Q. intros [b' j]. rewrite h in j. destruct j as [j1 j2]. auto. match goal with [|- ε ?x = _] => set (Q := x); set (q := ε Q) end. assert (i : exists b, Q b). exists b. exists a. reflexivity. generalize (ε_spec i). fold q. unfold Q. intros [a' j]. rewrite h in j. destruct j as [j1 j2]. auto. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat