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 : ...