Another bug.

diff --git a/helm/software/matita/library/didactic/exercises/natural_deduction.ma b/helm/software/matita/library/didactic/exercises/natural_deduction.ma
index 2fef599e780e0da2e6d8dbeaa8c36448c140db59..c26fcb6e88d0585ee07340a0b3839ab5cc39a571 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,7 @@ theorem demorgan : ¬(A ∧ B) ⇒ ¬A ∨ ¬B.
 apply rule (prove (¬(A ∧ B) ⇒ ¬A ∨ ¬B));
 apply rule (⇒_i [H] (¬A ∨ ¬B));
 apply rule (RAA [K] (⊥));
-apply rule (¬_e (¬(¬A ∨ ¬B)) (¬A ∨ ¬C));
-       [ apply rule (discharge [H]).
-       |
+apply rule (¬_e (¬(¬A ∨ ¬B)) (¬A ∨ ¬B));
+       [ apply rule (discharge [K]).
+       | apply rule (∨_i_l (¬A));
        ]