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

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 bb67cd325..0f80c9772 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-.