Intuitionistic Propositional Logic

Lemma and_assoc : forall A B C:Prop, A /\ (B /\ C) -> (A /\ B) /\ C.

Lemma and_imp_dist : forall A B C D:Prop,
                     (A -> B) /\ (C -> D) -> A /\ C -> B /\ D.

Lemma not_contrad : forall A : Prop, ~(A /\ ~A).

Lemma or_and_not : forall A B : Prop, (A\/B)/\~A -> B.

Solution

Note