Variable A,B,C:Prop. Variable U:Set. Variable a,b,c,d:U. Variable P,Q,R,S,F,G,J,I,K:U->Prop. Variable Fp, Gp, Hp : U -> U -> Prop. Lemma e1 : (x:U) (P x) -> (EX x:U | (P x)). Proof. Intros. Exists x. Assumption. Qed. Lemma e2 : A \/ ((x:U) (P x)) -> (x:U) A \/ (P x). Proof. Intro. Elim H. Intros. Left . Assumption. Intro. Intro. Right . Apply H0. Qed. Lemma e23 : a=b \/ c=d -> a=c \/ b=d -> a=d \/ b=c. Proof. Intros. Elim H. Intro. Elim H0. Intro. Right . Rewrite <- H1. Assumption. Intro. Left . Rewrite H1. Assumption. Intro. Elim H0. Intro. Left . Rewrite <- H1. Assumption. Intro. Right . Rewrite H1. Assumption. Qed. Lemma e10 : ((x:U) (F x) /\ ((G x) \/ (K x)) -> (I x)) -> ((x:U) (I x) /\ (K x) -> (J x)) -> ((x:U) (P x) -> (K x)) -> (x:U) (F x) /\ (P x) -> (J x). Proof. (*@*) Intros. Apply H0. Elim H2. Intros. Split. Apply H. Split. Assumption. Right . Apply H1. Assumption. Apply H1. Assumption. Qed. Lemma e11 : ((x:U) (F x) /\ ((G x) \/ (K x)) -> (I x)) -> ((x:U) (I x) /\ (K x) -> (J x)) -> ((x:U) (P x) -> (K x)) -> (x:U) (F x) /\ (P x) -> (J x). Proof. (*@*) Intros. Apply H0. Split. Apply H. Elim H2. Intros. Split. Assumption. Right . Apply H1. Assumption. Apply H1. Elim H2. Trivial. Qed. Lemma e14 : (p:Prop) ~(p <-> ~p). Proof. (*@@*) Unfold not. Intros. Elim H. Intros. Cut p->False. Intro. Apply H2. Apply H1. Assumption. Intro. Apply H0. Assumption. Assumption. Qed. Lemma e5 : ((x:U) (P x) -> (y:U) (Q y)) -> (((x:U) (Q x) \/ (R x)) -> (EX x:U | (Q x) /\ (S x))) -> ((EX x:U | (S x)) -> (x:U) (F x) -> (G x)) -> (x:U) (P x) /\ (F x) -> (G x). Proof. (*@@*) Intros. Apply H1. Elim H2. Intros. Cut (EX x:U | (Q x)/\(S x)). Intro. Elim H5. Intros. Exists x0. Elim H6. Intros. Assumption. Apply H0. Intros. Left . Apply H with x:=x. Assumption. Elim H2. Intros. Assumption. Qed. Lemma e6 : (EX x:U | (F x) /\ ~(G x)) -> ((x:U) (F x) -> (G x)) -> ((x:U) (J x) /\ (I x) -> (F x)) -> ((EX x:U | (K x) /\ ~(G x)) -> (x:U) (I x) -> ~(K x)) -> (x:U) (J x) -> ~(I x). Proof. (*@@*) Intros. Elim H. Intros. Elim H4. Intros. Absurd (G x0). Assumption. Apply H0. Assumption. Qed. Lemma e7 : (EX x:U | (F x)) /\ (EX x:U | (G x)) -> (((x:U) (F x) -> (K x)) /\ ((x:U) (G x) -> (J x)) <-> (x,y:U) (F x) /\ (G y) -> (K x) /\ (J y)). Proof. (*@@*) Intro. Elim H. Intros. Elim H0. Intros. Elim H1. Intros. Split. Intros. Elim H4. Intros. Elim H5. Intros. Split. Apply H6. Assumption. Apply H7. Assumption. Intros. Split. Intros. Cut (K x1)/\(J x0). Intro. Elim H6. Intros. Assumption. Apply H4. Split. Assumption. Assumption. Intros. Cut (K x)/\(J x1). Intro. Elim H6. Intros. Assumption. Apply H4. Split. Assumption. Assumption. Qed. Lemma e9 : ~(EX x:U | (F x) /\ ((G x) \/ (K x))) -> (EX x:U | (I x) /\ (F x)) -> ((x:U) (K x) \/ (J x)) -> (EX x:U | (I x) /\ (J x)). Proof. (*@@*) Intros. Elim H0. Intros. Elim H2. Intros. Elim (H1 x). Intro. Cut (EX x:U | (F x)/\((G x)\/(K x))). Intro. Elim (H H6). Exists x. Split. Assumption. Right . Assumption. Intro. Exists x. Split. Assumption. Assumption. Qed. Lemma e12 : ((x:U) (EX y:U | (Fp x y))) -> ((x:U) (EX y:U | (Gp x y))) -> ((x,y:U) (Fp x y) \/ (Gp x y) -> (z:U) (Fp y z) \/ (Gp y z) -> (Hp x z)) -> (x:U) (EX y:U | (Hp x y)). Proof. (*@@*) Intros. Elim (H x). Intros. Elim (H0 x0). Intros. Exists x1. Apply H1 with y:=x0. Left . Assumption. Right . Assumption. Qed. Lemma e15 : ~(EX x:U | (y:U) (Fp y x) <-> ~(Fp y y)). Proof. (*@@*) (* necessite e14 *) Unfold 1 not. Intro. Elim H. Intros. Cut (Fp x x)<->~(Fp x x). Exact (e14 (Fp x x)). Apply H0. Qed. Lemma e17 : ((z:U) (EX y:U | (x:U) (Fp x y) <-> (Fp x z) /\ ~(Fp x x))) -> ~(EX z:U | (x:U) (Fp x z)). Proof. (*@@*) Unfold 2 not. Intros. Elim H0. Intros. Elim (H x). Intros. Cut ~((Fp x0 x0)<->(Fp x0 x)/\~(Fp x0 x0)). Intro. Elim (H3 (H2 x0)). Unfold 1 not. Intro. Cut (Fp x0 x0)<->~(Fp x0 x0). Exact (e14 (Fp x0 x0)). Elim H3. Intros. Split. Intro. Cut (Fp x0 x)/\~(Fp x0 x0). Intro. Elim H7. Trivial. Apply H4. Assumption. Intro. Apply H5. Split. Apply H1. Assumption. Qed. Lemma e20 : ((x:U) (F x) -> (EX y:U | (G y) /\ (Hp x y)) /\ (EX y:U | (G y) /\ ~(Hp x y))) -> (EX x:U | (J x) /\ (y:U) (G y) -> (Hp x y)) -> (EX x:U | (J x) /\ ~(F x)). Proof. (*@@*) Intros. Elim H0. Intros. Elim H1. Intros. Exists x. Split. Assumption. Unfold not. Intro. Elim (H x H4). Intros. Elim H6. Intros. Elim H7. Intros. Absurd (Hp x x0). Assumption. Apply H3. Assumption. Qed. Lemma e24 : (EX x:U | (EX y:U | (z:U) z=x \/ z=y)) -> (P a) /\ (P b) -> ~a=b -> (x:U) (P x). Proof. (*@@*) Intros. Elim H0. Intros. Elim H. Intros. Elim H4. Intros. Elim (H5 a). Intro. Elim (H5 b). Intro. Rewrite H6 in H1. Rewrite H7 in H1. Absurd x0=x0. Assumption. Reflexivity. Intro. Rewrite <- H6 in H5. Rewrite <- H7 in H5. Elim (H5 x). Intro. Rewrite H8. Assumption. Intro. Rewrite H8. Assumption. Intro. Elim (H5 b). Intro. Rewrite <- H6 in H5. Rewrite <- H7 in H5. Elim (H5 x). Intro. Rewrite H8. Assumption. Intro. Rewrite H8. Assumption. Intro. Rewrite H6 in H1. Rewrite H7 in H1. Absurd x1=x1. Assumption. Reflexivity. Qed. Lemma e3 : (EX x:U | (P x)) -> ((x:U) (F x) -> ~(G x) /\ (R x)) -> ((x:U) (P x) -> (G x) /\ (F x)) -> ((x:U) (P x) -> (Q x)) \/ (EX x:U | (P x) /\ (R x)) -> (EX x:U | (Q x) /\ (P x)). Proof. (*@@@*) Intros. Elim H. Intros. Cut (G x)/\(F x). Intro. Cut ~(G x)/\(R x). Intro. Elim (proj1 ? ? H5 (proj1 ? ? H4)). Apply H0. Exact (proj2 ? ? H4). Apply H1. Assumption. Qed. (* Ou: Intros. Elim H2. Intro. Elim H. Intros. Exists x. Split. Apply H3. Assumption. Assumption. Intro. Elim H3. Intros. Elim H4. Intros. Exists x. Split. Absurd (G x). Cut ~(G x)/\(R x). Intro. Elim H7. Intros. Assumption. Apply H0. Cut (G x)/\(F x). Intro. Elim H7. Intros. Assumption. Apply H1. Assumption. Cut (G x)/\(F x). Intro. Elim H7. Intros. Assumption. Apply H1. Assumption. Assumption. *) (* Ou: Intros. Elim H2. Intro. Elim H. Intros. Exists x. Exact (conj ? ? (H3 x H4) H4). Intro. Elim H3. Intros. Elim H4. Intros. Exists x. Split. Cut (G x). Intro. Cut (F x). Intro. Cut ~(G x). Intro. Elim (H9 H7). Exact (proj1 ? ? (H0 x H8)). Exact (proj2 ? ? (H1 x H5)). Exact (proj1 ? ? (H1 x H5)). Assumption. *) Lemma e4 : ((EX x:U | (P x)) <-> (EX x:U | (Q x))) -> ((x,y:U) (P x) /\ (Q y) -> ((R x) <-> (S y))) -> (((x:U) (P x) -> (R x)) <-> (x:U) (Q x) -> (S x)). Proof. (*@@@*) Intros. Elim H. Intros. Split. Intros. Cut (EX y:U | (P y)). Intro. Elim H5. Intros. Cut (R x0)<->(S x). Intro. Elim H7. Intros. Apply H8. Apply H3. Assumption. Apply H0. Split. Assumption. Assumption. Apply H2. Exists x. Assumption. Intros. Cut (EX y:U | (Q y)). Intro. Elim H5. Intros. Cut (R x)<->(S x0). Intro. Elim H7. Intros. Apply H9. Apply H3. Assumption. Apply H0. Split. Assumption. Assumption. Apply H1. Exists x. Assumption. Qed. Lemma e8 : ((x:U) (F x) \/ (G x) -> ~(K x)) -> ((x:U) (I x) \/ ~(I x)) -> ((x:U) ((G x) -> ~(I x)) -> (F x) /\ (K x)) -> (x:U) (I x). Proof. (*@@@*) Intros. Elim (H0 x). Trivial. Intro. Absurd (K x). Apply H. Left . Cut (F x)/\(K x). Intro. Elim H3. Trivial. Apply H1. Intro. Assumption. Cut (F x)/\(K x). Intro. Elim H3. Trivial. Apply H1. Intro. Assumption. Qed. Lemma e16 : (EX y:U | (x:U) (Fp x y) <-> (Fp x x)) -> ~(x:U) (EX y:U | (z:U) (Fp z y) <-> ~(Fp z x)). Proof. (*@@@*) Unfold 1 not. Intros. Elim H. Intros. Elim (H0 x). Intros. Cut (Fp x0 x0)<->~(Fp x0 x). Intro. Cut (Fp x0 x)<->~(Fp x0 x). Exact (e14 (Fp x0 x)). Elim H3. Intros. Elim (H1 x0). Intros. Split. Intro. Apply H4. Apply H6. Assumption. Intro. Apply H7. Apply H5. Assumption. Apply H2. Qed. Lemma e19 : ((x,y:U) (Gp x y) <-> (z:U) (Fp z x) <-> (Fp z y)) -> (x,y:U) (Gp x y) <-> (Gp y x). Proof. (*@@@*) Intros. Elim (H x y). Intros. Elim (H y x). Intros. Split. Intro. Apply H3. Intro. Elim (H0 H4 z). Intros. (Split; Assumption). Intro. Apply H1. Intro. Elim (H2 H4 z). Intros. (Split; Assumption). Qed. Lemma e21 : ((x:U) (F x) /\ ((y:U) (G y) /\ (Hp x y) -> (Fp x y)) -> (y:U) (G y) /\ (Hp x y) -> (P y)) -> ~(EX y:U | (Q y) /\ (P y)) -> (EX x:U | (F x) /\ ((y:U) (Hp x y) -> (Q y)) /\ ((y:U) (G y) /\ (Hp x y) -> (Fp x y))) -> (EX x:U | (F x) /\ ~(EX y:U | (G y) /\ (Hp x y))). Proof. (*@@@*) Intros. Elim H1. Intros. Elim H2. Intros. Elim H4. Intros. Exists x. Split. Assumption. Unfold not. Intro. Elim H7. Intros. Elim H8. Intros. Cut (Q x0). Intro. Cut (P x0). Intro. Cut (EX y:U | (Q y)/\(P y)). Intro. Apply H0. Assumption. Exists x0. (Split; Assumption). Apply H with x:=x. Split. Assumption. Exact H6. Assumption. Apply H5. Assumption. Qed. Lemma e25 : (EX z:U | (EX w:U | (x,y:U) (Fp x y) <-> (x=z /\ y=w))) -> (EX z:U | (x:U) (EX w:U | (y:U) (Fp x y) <-> y=w) <-> x=z). Proof. (*@@@*) Intro. Elim H. Intros. Elim H0. Intros. Exists x. Intro. Split. Intro. Elim H2. Intros. Cut x1=x/\x2=x0. Intro. Elim H4. Trivial. Cut (Fp x1 x2)<->x1=x/\x2=x0. Intro. Elim H4. Intros. Apply H5. Cut (Fp x1 x2)<->x2=x2. Intro. Elim H7. Intros. Apply H9. Reflexivity. Apply H3. Apply H1. Intro. Exists x0. Intro. Split. Intro. Cut x1=x/\y=x0. Intro. Elim H4. Trivial. Cut (Fp x1 y)<->x1=x/\y=x0. Intro. Elim H4. Intros. Apply H5. Assumption. Apply H1. Intro. Cut (Fp x1 y)<->x1=x/\y=x0. Intro. Elim H4. Intros. Apply H6. Split. Assumption. Assumption. Apply H1. Qed. Lemma e13 : ((z:U) (EX w:U | (x:U) (EX y:U | ((Fp x z) -> (Fp y w)) /\ (Fp y z) /\ ((Fp y w) -> (EX u:U | (Gp u w)))))) -> ((x,z:U) (Fp x z) \/ (EX y:U | (Gp y z))) -> ((EX x:U | (EX y:U | (Gp x y))) -> (x:U) (Hp x x)) -> (x:U) (EX y:U | (Hp x y)). Proof. (*@@@@*) Intros. Exists x. Apply H1. Elim (H x). Intros. Elim (H2 x).Intros. Elim (H0 x x). Intro. Elim H3. Intros. Elim H6. Intros. Cut (EX u:U | (Gp u x0)). Intro. Elim H9. Intros. Exists x2. Exists x0. Assumption. Apply H8. Apply H5. Assumption. Intro. Elim H4. Intros. Exists x2. Exists x. Assumption. Qed. (* Lemma e18 : ~(EX y:U | (x:U) (Fp x y) <-> ~(EX z:U | (Fp x z) /\ (Fp z x))). *) (* Lemma e22 : ((x:U) ((F x) /\ (y:U) (F y) /\ (Hp y x) -> (G y)) -> (G x)) -> ((EX x:U | (F x) /\ ~(G x)) -> (EX x:U | (F x) /\ ~(G x) /\ (y:U) (F y) /\ ~(G y) -> (Fp x y))) -> ((x,y:U) (F x) /\ (F y) /\ (Hp x y) -> ~(Fp y x)) -> (x:U) (F x) -> (G x). *) (* Lemma e26 : (EX z:U | (EX w:U | (x,y:U) (Fp x y) <-> (x=z /\ y=w))) -> (EX w:U | (y:U) (EX z:U | (x:U) (Fp x y) <-> x=z) <-> y=w). *) (* Lemma e27 : ((y:U) (EX z:U | (x:U) (Fp x z) <-> x=y)) -> ~(EX w:U | (x:U) (Fp x w) <-> (u:U) (Fp x u) -> (EX y:U | (Fp y u) /\ ~(EX z:U | (Fp z u) /\ (Fp z y)))). *)