partial update in static_2

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / syntax / sd_lt.ma

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 23725dba7544c109e848565422f7bd71571cc835..24d4651b5f2bab5267c56bde4c2f7f5c4ce5796d 100644 (file)
--- 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.