(* Forward lemmas with free variables inclusion for restricted closures *****)
lemma req_rex_trans: ∀R. req_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 req_fsle_comp, rex_trans_fsle, rex_trans_next/ qed-.