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=23725dba7544c109e848565422f7bd71571cc835;hp=238d1a28b60a5ddae2fb4055dd63971e59e88aa9;hb=98e786e1a6bd7b621e37ba7cd4098d4a0a6f8278;hpb=5d9f7ae4bad2b5926f615141c12942b9a8eb23fb

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 238d1a28b..23725dba7 100644
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/sd_lt.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/sd_lt.ma
@@ -23,10 +23,10 @@ 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
-  elim (lt_refl_false … Hs12)
+  elim (nlt_inv_refl … Hs12)
 | #n #H
-  lapply (next_lt … Hh ((next h)^n s2)) >H -H #H
-  lapply (transitive_lt … H Hs12) -s1 #H1
-  /3 width=5 by lt_le_false, nexts_le/ (* full auto too slow *)
+  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 *)
 ]
 qed.