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)).

Lemma e2 : A \/ ((x:U) (P x)) -> (x:U) A \/ (P x).

Lemma e23 : a=b \/ c=d -> a=c \/ b=d -> a=d \/ b=c.

(* @ *)

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).

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).

(* @@ *)

Lemma e14 : (p:Prop) ~(p <-> ~p).

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).

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).

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)).

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)).

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)).

Lemma e15 : ~(EX x:U | (y:U) (Fp y x) <-> ~(Fp y y)).

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)).

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)).

Lemma e24 : (EX x:U | (EX y:U | (z:U) z=x \/ z=y)) ->
            (P a) /\ (P b) ->
	    ~a=b ->
              (x:U) (P x).

(* @@@ *)

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)).

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)).

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).

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)).

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).

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))).

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).

(* @@@@ *)

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)).