X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fmodels%2Fnat_dedekind_sigma_complete.ma;h=0908b6f7079ae8f2acf97cfac5758717b3124054;hb=ada8695ba51b2ecbd4a955f990e8d06f038aac6b;hp=04b861d41cea7e497feb7be6dfcfbc5f881a019d;hpb=7e33e23e18dc5d008b3b3dc0052aa4d7b236415e;p=helm.git

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 04b861d41..0908b6f70 100644
--- 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]