This commit shows a bug.

diff --git a/helm/software/matita/library/didactic/exercises/natural_deduction.ma b/helm/software/matita/library/didactic/exercises/natural_deduction.ma
index 8ec8d6fd74407326538e3f780b86f53fe32f95d2..2fef599e780e0da2e6d8dbeaa8c36448c140db59 100644 (file)
--- a/helm/software/matita/library/didactic/exercises/natural_deduction.ma
+++ b/helm/software/matita/library/didactic/exercises/natural_deduction.ma
@@ -21,6 +21,10 @@ include "didactic/support/natural_deduction.ma".
 
 
 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]).
+       |
+       ]