Load CS3202.

(* ======================
  First Part *)

Variable iota:Set.

(* Check out how I declare in a single command
 several variables of the same type, mind the 's' *)

Variables P Q:iota->Prop.


Conjecture t1:(forall x, P x->Q x)->((forall y, P y)->(forall z, Q z)).
(* Turn "Conjecture" into "Theorem"
   and complete the proof in Coq's proof-mode *)

Print t1.
Eval compute in t1.

Conjecture t2: (exists x,P x \/ Q x)->(exists y, P y)\/(exists z, Q z).
(* Turn "Conjecture" into "Theorem"
   and complete the proof in Coq's proof-mode *)

Print t2.
Eval compute in t2.

Conjecture t3: ((exists y, P y)\/(exists z, Q z)) -> (exists x,P x \/ Q x).
(* Turn "Conjecture" into "Theorem"
   and complete the proof in Coq's proof-mode *)

Print t3.
Eval compute in t3.

(* ======================
  Second Part *)

Definition LEM (D:Prop) := D\/~D.
Definition Peirce (A B: Prop) := ((A->B)->A)->A.
Definition EDN (C:Prop) := (~~C)->C.

Variables E F:Prop.

Conjecture one : EDN E->Peirce E F.

(* Turn "Conjecture" into "Theorem"
   and complete the proof in Coq's proof-mode *)

Print one.
Eval compute in one.

Conjecture two : Peirce (E\/~E) False ->LEM E.

(* Turn "Conjecture" into "Theorem"
   and complete the proof in Coq's proof-mode *)

Print two.
Eval compute in two.

Conjecture three : LEM E->EDN E.

(* Turn "Conjecture" into "Theorem"
   and complete the proof in Coq's proof-mode *)

Print three.
Eval compute in three.