+lemma distr_and_or_l : ∀A,B,C:Prop. A ∧(B ∨ C) → (A ∧ B) ∨ (A ∧ C).
+#A #B #C * #H *
+ [#H1 %1 % [@H |@H1] |#H1 %2 % //]
+qed.
+
+lemma distr_and_or_r : ∀A,B,C:Prop. (A ∧ B) ∨ (A ∧ C) → A ∧ (B ∨ C).
+#A #B #C * * #H1 #H2
+ [% [// | %1 //] | % [// | %2 //]
+qed.
+
+
+lemma distr_or_and_l : ∀A,B,C:Prop. A ∨(B ∧ C) → (A ∨ B) ∧ (A ∨ C).
+#A #B #C *
+ [#H % [%1 // |%1 //] | * #H1 #H2 % [%2 // | %2 //] ]
+qed.
+
+lemma distr_or_and_r : ∀A,B,C:Prop. (A ∨ B) ∧ (A ∨ C) → A ∨ (B ∧ C).
+#A #B #C
+* * #H * /3/
+qed.
+
+definition neg ≝ λA:Prop. A → False.
+
+lemma neg_neg : ∀A. A → neg (neg A).
+#A #H normalize #H1 @(H1 H)
+qed.