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=75f395f0febd02de8e0f881d918a8812b1425c8d;hp=bb67cd3254a57b9a853704a05da6aab88a87bd99;hpb=d59f344b1e4b377e2f06abd9f8856d686d21b222;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-.