Require Import Bool Arith List.

Variables P Q R : Prop.

(* 5. Write the script that proves the following formula
   (P -> (P /\ Q) -> R) -> P /\ (Q /\ P) -> R. *)

Lemma ex5 :
   (P -> (P /\ Q) -> R) -> P /\ (Q /\ P) -> R.
Proof.
...
Qed.

(* 7. Write the script that proves the following formula
     (P /\ Q) \/ R -> P \/ R *)

Lemma ex7 : ...


(* 7. Write the script that proves the following formula
   ((P -> Q \/ P) -> R) -> R \/ Q  *)

Lemma ex8 : ...