Section simple_proofs. Variables P Q R S : Prop. Lemma id_P : P -> P. Proof. intro; assumption. Qed. Lemma id_PP : (P -> P) -> P -> P. Proof. intro; assumption. Qed. Lemma imp_trans : (P -> Q) -> (Q -> R) -> P -> R. Proof. intros H H0 p. apply H0; apply H; assumption. Qed. Lemma imp_perm : (P -> Q -> R) -> Q -> P -> R. Proof. intros H q p; apply H; assumption. Qed. Lemma ignore_Q : (P -> R) -> P -> Q -> R. Proof. intros H p q; apply H; assumption. Qed. Lemma delta_imp : (P -> P -> Q) -> P -> Q. Proof. intros H p; apply H; assumption. Qed. Lemma delta_impR : (P -> Q) -> P -> P -> Q. Proof. intros H p p'; apply H; assumption. Qed. Lemma diamond : (P -> Q) -> (P -> R) -> (Q -> R -> S) -> P -> S. Proof. intros H H0 H1 p. apply H1; [ apply H | apply H0 ]; assumption. Qed. Lemma weak_peirce : ((((P -> Q) -> P) -> P) -> Q) -> Q. Proof. intro H; apply H. intro H0; apply H0. intro p; apply H; intro; assumption. Qed. End simple_proofs.