Section PropLogic. 

Variables A, B, C : Prop.

(* Example *)
Lemma LS : (A->(B->C))->(A->B)->(A->C).
Intros x y z. (* Intros. *)
Apply x. 
Assumption.  (* Exact z. *)
Apply y.
Assumption. (* Exact z *)
Qed.

(* Exercise 2 *)

Lemma ex2a: (A->B)->(B->C)->A->C.
Abort.
(* Qed. Print ex1a. *)

Lemma ex2b: ((A->B->A)->A)->A.
Abort.
(* Qed. Print ex1a. *)

(* Exercise 1 *)
Definition T1 := ...
Definition T2 := ...
Definition ex1a := [x:T1][y:T2]((y x) x).

Definition T3 := ...
Definition ex1b := [x:T1][y:T2](x ([z:T3]y) y).

(* Exercise 3 *)
Definition ex3a := [x:?][y:?][z:?](x z (y z)).

Definition ex3b' := [x:?][y:?]x.

Definition ex3b'' := [x:?][y:?]x.

Definition ex3c := (ex3a ex3b' ex3b'') : ?

Definition ex3d := [x:?]x

(* Exercise 4 *)
(* Ex 4a *x)
Definition NAT := A->(A->A)->A.
Definition zero := ? : NAT. 
Definition one := ? : NAT. 
Definition two := ? : NAT. 

Definition succ := ? : NAT -> NAT.

(* Ex 4c *)
Definition der:= ? : ((A->B)->C) -> (B->C).

Print der.