X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdidactic%2Fexercises%2Fnatural_deduction.ma;fp=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdidactic%2Fexercises%2Fnatural_deduction.ma;h=1bc9717fd5ec7966d41efcf09d674705955e012d;hb=2030cae5f1a588fa6bbea50927030f83a2156d67;hp=7f941c1189ed34d408ace19df731848b1007f895;hpb=f870943aedc6ef6f51be134ed3e82bbc03b3eea1;p=helm.git

diff --git a/helm/software/matita/library/didactic/exercises/natural_deduction.ma b/helm/software/matita/library/didactic/exercises/natural_deduction.ma
index 7f941c118..1bc9717fd 100644
--- a/helm/software/matita/library/didactic/exercises/natural_deduction.ma
+++ b/helm/software/matita/library/didactic/exercises/natural_deduction.ma
@@ -173,7 +173,7 @@ apply rule (⇒_i [h2] ((D ⇒ A) ⇒ D ⇒ C));
 apply rule (⇒_i [h3] (D ⇒ C));
 apply rule (⇒_i [h4] (C));
 apply rule (∨_e (B∨¬B) [h5] (C) [h6] (C));
-	[ apply rule (lem EM);
+	[ apply rule (lem 0 EM);
 	| apply rule (⇒_e (B∧D⇒C) (B∧D));
 	    [ apply rule (discharge [h2]);
     	| apply rule (∧_i (B) (D));
@@ -234,9 +234,9 @@ apply rule (prove (¬(A∧B) ⇒ ¬A∨¬B));
 (*BEGIN*)
 apply rule (⇒_i [h1] (¬A∨¬B));
 apply rule (∨_e (A ∨ ¬A) [h2] ((¬A∨¬B)) [h3] ((¬A∨¬B)));
-	[ apply rule (lem EM);
+	[ apply rule (lem 0 EM);
 	| apply rule (∨_e (B ∨ ¬B) [h4] ((¬A∨¬B)) [h5] ((¬A∨¬B)));
-	    [ apply rule (lem EM);
+	    [ apply rule (lem 0 EM);
 	    | apply rule (⊥_e (⊥));
 	      apply rule (¬_e (¬(A∧B)) (A∧B));
 	        [ apply rule (discharge [h1]);
@@ -259,7 +259,7 @@ apply rule (prove (¬(A∨B) ⇒ (¬A ∧ ¬B)));
 (*BEGIN*)
 apply rule (⇒_i [h1] (¬A ∧ ¬B));
 apply rule (∨_e (A∨¬A) [h2] (¬A ∧ ¬B) [h3] (¬A ∧ ¬B));
-	[ apply rule (lem EM);
+	[ apply rule (lem 0 EM);
 	| apply rule (⊥_e (⊥));
     apply rule (¬_e (¬(A∨B)) (A∨B));
 	    [ apply rule (discharge [h1]);
@@ -267,7 +267,7 @@ apply rule (∨_e (A∨¬A) [h2] (¬A ∧ ¬B) [h3] (¬A ∧ ¬B));
         apply rule (discharge [h2]);
 	    ]
 	| apply rule (∨_e (B∨¬B) [h10] (¬A ∧ ¬B) [h11] (¬A ∧ ¬B));
-	    [ apply rule (lem EM);
+	    [ apply rule (lem 0 EM);
 	    | apply rule (⊥_e (⊥));
         apply rule (¬_e (¬(A∨B)) (A∨B));
 	        [ apply rule (discharge [h1]);
@@ -318,5 +318,5 @@ apply rule (⇒_e ((A⇒⊥)⇒⊥) (A⇒⊥));
 	    ]
 	]
 (*END*)
-qed. 
+qed.