X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fsyntax%2Fsd_lt.ma;h=24d4651b5f2bab5267c56bde4c2f7f5c4ce5796d;hp=23725dba7544c109e848565422f7bd71571cc835;hb=8fe4dc148d50a0352313633bea61441bc817afbf;hpb=cab35e3d6c09d266c1372b5cc9a0045578bae79b

diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/sd_lt.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/sd_lt.ma
index 23725dba7..24d4651b5 100644
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/sd_lt.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/sd_lt.ma
@@ -20,13 +20,14 @@ include "static_2/syntax/sd_d.ma".
 (* Properties with sh_lt ****************************************************)
 
 lemma deg_SO_gt (h): sh_lt h →
-      ∀s1,s2. s1 < s2 → deg_SO h s1 s2 0.
-#h #Hh #s1 #s2 #Hs12 @deg_SO_zero * normalize
-[ #H destruct
+      ∀s1,s2. s1 < s2 → deg_SO h s1 s2 𝟎.
+#h #Hh #s1 #s2 #Hs12 @deg_SO_zero
+#n @(nat_ind_succ … n) -n
+[ <sh_nexts_zero #H destruct
   elim (nlt_inv_refl … Hs12)
-| #n #H
-  lapply (next_lt … Hh ((pr_next h)^n s2)) >H -H #H
-  lapply (nlt_trans … H Hs12) -s1 #H1
-  /3 width=5 by nlt_ge_false, nexts_le/ (* full auto too slow *)
+| #n #_ <sh_nexts_succ #H
+  lapply (sh_next_lt h Hh (⇡*[h,n]s2)) >H -H #H
+  lapply (nlt_trans … H … Hs12) -s1 #H1
+  /3 width=5 by nlt_ge_false, sh_nexts_le/ (* full auto too slow *)
 ]
 qed.