]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/static/lfeq_fsle.ma
update in basic_2 + web page
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / static / lfeq_fsle.ma
index 0f80c977289f687fb8d248bb612c443df284c606..bb67cd3254a57b9a853704a05da6aab88a87bd99 100644 (file)
@@ -29,5 +29,5 @@ qed.
 (* Forward lemmas with free variables inclusion for restricted closures *****)
 
 lemma lfeq_lfxs_trans: ∀R. lfeq_transitive R →
-                       â\88\80L1,L,T. L1 â\89¡[T] L → ∀L2. L ⪤*[R, T] L2 → L1 ⪤*[R, T] L2.
+                       â\88\80L1,L,T. L1 â\89\90[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-.