apply rule (lem EM) works

[helm.git] / helm / software / matita / library / didactic / exercises / natural_deduction.ma

diff --git a/helm/software/matita/library/didactic/exercises/natural_deduction.ma b/helm/software/matita/library/didactic/exercises/natural_deduction.ma
index 7d4e1ff11ca5ae0a0828c707933425c04217347e..de1c1f482cf91cd1cafbd54565cd119ae9c974df 100644 (file)
--- a/helm/software/matita/library/didactic/exercises/natural_deduction.ma
+++ b/helm/software/matita/library/didactic/exercises/natural_deduction.ma
@@ -24,7 +24,8 @@ 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 (⊥_e (⊥));
+         apply rule (¬_e (¬¬A) (¬A));
           [ apply rule (¬_i [K] (⊥)).
        apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
              [ apply rule (discharge [H]).
@@ -58,6 +59,14 @@ apply rule (¬_e (¬(¬A ∨ ¬B)) (¬A ∨ ¬B));
                 | apply rule (discharge [M]).
                 ]
              ]
-          | apply rule EM;
+          | apply rule (∨_e (B ∨ ¬B) [h1] (B) [h2] (B));
+              [ apply rule (lem EM);
+              
+
+              | apply rule (discharge [h1]);
+              |
+              ]
+ 
+          apply rule (show EM);
           ]
        ]