Variable obj : Set.

Variable P2 :  Prop.

Lemma l3 : (exists x : obj, P2) -> P2.
intuition.
elim H.
intros.
auto.
Qed.

Variable Q : obj -> Prop.
Variable P : obj -> Prop.
Variable q : obj.

Lemma remove_ex : (forall P : Prop, (exists x : obj, P) -> P).
intro.
intuition.
elim H.
intros.
auto.
Qed.



Lemma spl : (forall P  Q : obj -> Prop,
(exists x : obj, P x /\ Q x) -> (exists x : obj, P x) /\ (exists x : obj, Q x)).
intro.
intro.
intro.
elim H.
split .
exists x.
tauto.
exists x.
tauto.
Qed.

Lemma l4 : (exists x : obj, P x \/ Q x) -> (exists x : obj, P x) \/ (exists x : obj, Q x).
intro.
elim H.
intro.
intro.
intuition.
constructor 1.
exists x.
trivial.
constructor 2.
exists x.
trivial.
Qed.

Lemma and_spl : (forall a a' b b' : Prop, 
(a -> a') -> (b -> b') -> (a /\ b -> a' /\ b')).
tauto.
Qed.

Lemma unskolem : forall T : Type, 
forall P : obj -> T -> Prop,
(exists f : obj -> T, forall y : obj, P y (f y)) ->
(forall y : obj, (exists x : T, P y x)).
intro. intro. intro. elim H. intro f. intro.
intro. exists (f y). apply H0.
Qed.

Lemma x42 : 
(exists f : obj -> obj -> obj, forall x : obj, forall y : obj, Q (f x y)) ->
forall x : obj, forall y : obj, exists z : obj, Q z.
intro.
intro.
apply unskolem.
apply unskolem with  
(P := fun (_ : obj) (fx :  obj -> obj) => forall y : obj, Q (fx y))
.
trivial.
trivial.
Qed.



Lemma x1: (exists f : obj -> obj, forall y : obj, (P(f y) /\ Q y)) ->
(forall y : obj, ((exists x : obj, P x) /\ Q y)).
intro.
assert (forall y : obj, (exists x : obj, P x /\ Q y)).
apply unskolem.
trivial.
intro.
assert ((exists x : obj, P x) /\ (exists x : obj, Q y)).
apply spl.
apply H0.
assert (ex (fun _ : obj => Q y) -> Q y).
apply remove_ex.
apply and_spl with 
(a := (exists x : obj, P x)) 
(a' := (exists x : obj, P x))
( b :=  (ex (fun _ : obj => Q y) ) )
(b' := Q y) .
intro. trivial.
trivial.
trivial.
Qed.

Variable Q2 : obj -> obj -> Prop.

Lemma x3: (exists x : obj, exists y : obj, Q2 x y) -> (exists y : obj, exists x : obj, Q2 x y).
intro.
elim H.
intro.
intro.
elim H0.
intro.
intro.
exists x0.
exists x.
trivial.
Qed.