(* 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-.