Section e3.

Variables X Y: Set.

Section a1.
Variables A: X -> Y -> Prop.

Lemma allcomm:
 (forall x:X, forall y:Y, A x y) <-> 
  forall y:Y, forall x:X, A x y.
Proof.
split.
intro lhs.
intro y0.
intro x0.
apply lhs.
intro rhs.
intro x1.
intro y1.
apply rhs.
Qed.
Print allcomm.
End a1.

Section a2.

Variables A: X-> Prop.
Variables B:  X->Prop.
Variables C:  X->Prop.

Lemma alltrans:
(forall x:X, A x -> B x) -> 
(forall x:X, B x -> C x) -> 
(forall x:X, A x -> C x).
Proof.
intro allAB.
intro allBC.
intro x.
intro Ax.
apply allBC.
apply allAB.
assumption.
Qed.

Print alltrans.
End a2.

Section a3.
Variables A: X-> Prop.
Variables B:  X->Prop.

Lemma ex_and:
(exists x: X, A x /\ B x)  ->  
(exists x:X, A x) /\ (exists x:X, B x).
Proof.
intro lhs.
elim lhs;intro x;intro H.
elim H;intro Ax; intro Bx.
split.
exists x.
assumption.
exists x;assumption.
Qed.
End a3.

Section a4.
Variables A: X -> Y -> Prop.

Lemma ex_all:
(exists x:X, forall y:Y, A x y)  ->  
forall y:Y, exists x:X, A x y.
Proof.
intro lhs.
intro y.
elim lhs;intro x; intro H.
exists x.
apply H.
Qed.

End a4.

Section a6.

Variables A: X-> Prop.
Variables B: Prop.

Lemma ex_impl:
(exists x:X, A x -> B)   ->   
(forall x:X, A x) -> B.
Proof.
intro lhs.
intro allAx.
elim lhs;intro x; intro H.
apply H.
apply allAx.
Qed.
End a6.


End e3.