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.