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.
Intros x y z.
Apply y.
Apply x.
Exact z.
Qed. 
Print ex2a.

Lemma ex2b: ((A->B->A)->A)->A.
Intro f.
Apply f.
Intros x y.
Exact x.
Qed. Print ex2b.

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

Definition T3 := (A->B)->B->C.
Definition T4 := B.
Definition T5 := A.
Definition ex1b := [x:T3][y:T4](x ([z:T5]y) y).

(* Exercise 3 *)
Definition ex3a := [x:A->(B->A)->A][y:A->B->A][z:A](x z (y z)).

Definition ex3b' := [x:A][y:B->A]x.

Definition ex3b'' := [x:A][y:B]x.

Definition ex3c := (ex3a ex3b' ex3b'') :A->A. 

Definition ex3d := [x:A]x : A->A.

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

Definition succ := [n:NAT][x:A][f:A->A](f(n x f)) : NAT -> NAT.
(* Alternatively: *)
Definition succ' := [n:NAT][x:A][f:A->A](n (f x) f) : NAT -> NAT.
(* Ex 4c *)
Definition der:= [f:(A->B)->C][x:B](f([z:A]x)) : ((A->B)->C) -> (B->C).

Print der.