new definition of lleq allows to complete the proof of lemma 1000

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / lsx_cpxs.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_cpxs.ma
index e6bf5d3e489658938043f0be4092eb6b7f925553..c877a9193195ff9b6bb5c51b6ea322fd9917acbc 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_cpxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_cpxs.ma
@@ -20,7 +20,7 @@ include "basic_2/computation/lsx.ma".
 (* Advanced properties ******************************************************)
 
 lemma lsx_lleq_trans: ∀h,g,T,G,L1. G ⊢ ⋕⬊*[h, g, T] L1 →
-                      ∀L2. L1 ⋕[0, T] L2 → G ⊢ ⋕⬊*[h, g, T] L2.
+                      ∀L2. L1 ⋕[T, 0] L2 → G ⊢ ⋕⬊*[h, g, T] L2.
 #h #g #T #G #L1 #H @(lsx_ind … H) -L1 #L1 #HL1 #IHL1 #L2 #HL12
 @lsx_intro #L #HL2 #HnT elim (lleq_lpxs_trans_nlleq … HL12 … HL2 HnT) -L2 /3 width=4 by/
 qed-.