- advances in the theory of cofrees

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

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 37f4edfaf3a8b0996e50f148dcf900a7dfafb908..d191024b9a8b35cc4da0118ae619f21cad4c8f20 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpx.ma
@@ -21,7 +21,7 @@ include "basic_2/computation/lsx.ma".
 (* Advanced properties ******************************************************)
 
 lemma lsx_lleq_trans: ∀h,g,T,G,L1,d. G ⊢ ⬊*[h, g, T, d] L1 →
-                      â\88\80L2. L1 â\8b\95[T, d] L2 → G ⊢ ⬊*[h, g, T, d] L2.
+                      â\88\80L2. L1 â\89¡[T, d] L2 → G ⊢ ⬊*[h, g, T, d] L2.
 #h #g #T #G #L1 #d #H @(lsx_ind … H) -L1
 #L1 #_ #IHL1 #L2 #HL12 @lsx_intro
 #K2 #HLK2 #HnLK2 elim (lleq_lpx_trans … HLK2 … HL12) -HLK2