Section Propositional_logic.

Section Basic_facts.

Variables P Q R T: Prop.

Lemma curry:
(P /\ Q -> R) -> (P -> Q -> R).
Proof.
intro H.
intro p.
intro q.
apply H.
split.
exact p.
exact q.
Qed.
Print curry.

Lemma and_commutative: 
P /\ Q -> Q /\ P.
Proof.
intro c.
split.
apply proj2 with P.
exact c.
apply proj1 with Q.
exact c.
Qed.
Print and_commutative.

Lemma and_associative:
(P /\ Q) /\ R -> P /\ (Q /\ R).
Proof.
intro c.
split.
apply proj1 with Q.
apply proj1 with R.
exact c.
split.
apply proj2 with P.
apply proj1 with R.
exact c.

Qed.
Print and_associative.

Lemma or_commutative: 
P \/ Q -> Q \/ P.
Proof.

Qed.
Print or_commutative.

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

Qed.
Print or_distr: