X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fcomputation%2Flsx_lpx.ma;h=034024b72ea8708b9ac9de822ca16618db0853b3;hb=52e675f555f559c047d5449db7fc89a51b977d35;hp=c4b2e04d518fc222a3f4df7a5f3c00e6554d8486;hpb=75fac6d60f67a4dfa38ea6c2cc45a18eda5d8996;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpx.ma
index c4b2e04d5..034024b72 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpx.ma
@@ -35,7 +35,7 @@ elim (lleq_dec T L1 L2 d) /3 width=4 by lsx_lleq_trans/
 qed-.
 
 lemma lsx_leq_conf: ∀h,g,G,L1,T,d. G ⊢ ⬊*[h, g, T, d] L1 →
-                    ∀L2. L1 ≃[d, ∞] L2 → G ⊢ ⬊*[h, g, T, d] L2.
+                    ∀L2. L1 ⩬[d, ∞] L2 → G ⊢ ⬊*[h, g, T, d] L2.
 #h #g #G #L1 #T #d #H @(lsx_ind … H) -L1
 #L1 #_ #IHL1 #L2 #HL12 @lsx_intro
 #L3 #HL23 #HnL23 elim (leq_lpx_trans_lleq … HL12 … HL23) -HL12 -HL23