Variables A B C D: Prop.

Theorem ex1_1: A->A.
intro.
apply H.
Qed.

Theorem ex1_2: (A->A)->(A->A).
intro.
intro.
apply H.
apply H0.
Qed.

Theorem ex1_3: (A->B)->(B->C)->(A->C).
intros.
apply H0.
apply H.
apply H1.
Qed.

Theorem ex1_4: (A->B)->A->C->B.
intros.
apply H.
apply H0.
Qed.

Theorem ex1_5: (A->B)->(A->C)->(B->C->D)->A->D.
intros.
apply H1.
apply H.
apply H2.
apply H0.
apply H2.
Qed.

Theorem ex1_6: ((((A->B)->A)->A)->B)->B.
intros.
apply H.
intros.
apply H0.
intros.
apply H.
intros.
apply H2.
intros.
apply H.
intros.
apply H1.
Qed.