New bug.

diff --git a/helm/software/matita/library/didactic/exercises/natural_deduction.ma b/helm/software/matita/library/didactic/exercises/natural_deduction.ma
index c26fcb6e88d0585ee07340a0b3839ab5cc39a571..7d4e1ff11ca5ae0a0828c707933425c04217347e 100644 (file)
--- a/helm/software/matita/library/didactic/exercises/natural_deduction.ma
+++ b/helm/software/matita/library/didactic/exercises/natural_deduction.ma
@@ -18,7 +18,28 @@
 
 include "didactic/support/natural_deduction.ma".
 
-
+theorem EM: ∀A. A ∨ ¬ A.
+assume A: CProp.
+apply rule (prove (A ∨ ¬A));
+apply rule (RAA [H] (⊥)).
+apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
+       [ apply rule (discharge [H]).
+       | apply rule (¬_e (¬¬A) (¬A));
+          [ apply rule (¬_i [K] (⊥)).
+       apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
+             [ apply rule (discharge [H]).
+             | apply rule (∨_i_r (¬A)).
+          apply rule (discharge [K]).
+             ]
+          | apply rule (¬_i [K] (⊥)).
+       apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
+             [ apply rule (discharge [H]).
+             | apply rule (∨_i_l (A)).
+          apply rule (discharge [K]).
+             ]
+          ]
+       ]
+qed.
 
 theorem demorgan : ¬(A ∧ B) ⇒ ¬A ∨ ¬B.
 apply rule (prove (¬(A ∧ B) ⇒ ¬A ∨ ¬B));
@@ -27,4 +48,16 @@ apply rule (RAA [K] (⊥));
 apply rule (¬_e (¬(¬A ∨ ¬B)) (¬A ∨ ¬B));
        [ apply rule (discharge [K]).
        | apply rule (∨_i_l (¬A));
+         apply rule (¬_i [L] (⊥)).
+         apply rule (¬_e (¬B) (B));
+          [ apply rule (¬_i [M] (⊥)).
+       apply rule (¬_e (¬(A ∧ B)) (A ∧ B));
+             [ apply rule (discharge [H]).
+             | apply rule (∧_i (A) (B));
+                [ apply rule (discharge [L]).
+                | apply rule (discharge [M]).
+                ]
+             ]
+          | apply rule EM;
+          ]
        ]