X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Flfeq_fsle.ma;h=bb67cd3254a57b9a853704a05da6aab88a87bd99;hp=0f80c977289f687fb8d248bb612c443df284c606;hb=268e7f336d036f77ffc9663358e9afda92b97730;hpb=1604f2ee65c57eefb7c6b3122eab2a9f32e0552d

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_fsle.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_fsle.ma
index 0f80c9772..bb67cd325 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_fsle.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_fsle.ma
@@ -29,5 +29,5 @@ qed.
 (* Forward lemmas with free variables inclusion for restricted closures *****)
 
 lemma lfeq_lfxs_trans: ∀R. lfeq_transitive R →
-                       ∀L1,L,T. L1 ≡[T] L → ∀L2. L ⪤*[R, T] L2 → L1 ⪤*[R, T] L2.
+                       ∀L1,L,T. L1 ≐[T] L → ∀L2. L ⪤*[R, T] L2 → L1 ⪤*[R, T] L2.
 /4 width=16 by lfeq_fsle_comp, lfxs_trans_fsle, lfxs_trans_next/ qed-.