- notation fixed according to the new stricter semantics

[helm.git] / helm / software / matita / contribs / dama / dama / models / nat_dedekind_sigma_complete.ma

diff --git a/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma b/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma
index 04b861d41cea7e497feb7be6dfcfbc5f881a019d..0908b6f7079ae8f2acf97cfac5758717b3124054 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma
+++ b/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma
@@ -52,11 +52,8 @@ letin m ≝ (hide ? (
    ∀i:nat.∃j:nat.spec i j));unfold spec in aux ⊢ %;
 [1: apply (H2 pred nP);
 |4: unfold X in H2; clear H4 n aux spec H3 H1 H X;
-    generalize in match H2;
-    generalize in match Hs;
-    generalize in match a;
-    clear H2 Hs a; cases u; intros (a Hs H);
-    [1: left; split; [apply le_n] 
+    cases u in H2 Hs a ⊢ %; intros (a Hs H);
+    [1: left; split; [apply le_n]
         generalize in match H;
         generalize in match Hs;
         rewrite > (?:s = O); 
@@ -68,7 +65,7 @@ letin m ≝ (hide ? (
         apply (trans_le ??? (os_le_to_nat_le ?? H1));
         apply le_plus_n_r;] 
 |2,3: clear H6;
-    generalize in match H5; clear H5; cases (aux n1); intros;
+    cases (aux n1) in H5 ⊢ %; intros;
     change in match (a 〈w,H5〉) in H6 ⊢ % with (a w);
     cases H5; clear H5; cases H7; clear H7;
     [1: left; split; [ apply (le_S ?? H5); | assumption]