Polymorphic minimal propositional logic

Lemma id_P : forall P:Prop, P -> P.

Lemma id_PP : forall P:Prop, (P -> P) -> P -> P.

Lemma imp_trans : forall P Q R :Prop, (P -> Q) -> (Q -> R) -> P -> R.

Lemma imp_perm :  forall P Q R :Prop, (P -> Q -> R) -> Q -> P -> R.

Lemma ignore_Q : forall P Q R :Prop, (P -> R) -> P -> Q -> R.

Lemma delta_imp :  forall P Q :Prop,(P -> P -> Q) -> P -> Q.

Lemma delta_impR :forall P Q :Prop, (P -> Q) -> P -> P -> Q.

Lemma diamond : forall P Q R T:Prop, (P -> Q) -> 
                                  (P -> R) -> 
                                  (Q -> R -> T) -> 
                                  P -> T.
Lemma weak_peirce : forall P Q:Prop, ((((P -> Q) -> P) -> P) -> Q) -> Q.

Solution