-(* Basic_2A1: uses: csx_lleq_conf *)
-lemma csx_reqx_trans: ∀h,L1,L2,T. L1 ≛[T] L2 →
- ∀G. ⦃G,L2⦄ ⊢ ⬈*[h] 𝐒⦃T⦄ → ⦃G,L1⦄ ⊢ ⬈*[h] 𝐒⦃T⦄.
+(* Basic_2A1: uses: csx_lleq_trans *)
+lemma csx_reqx_trans (h) (G) (L2):
+ ∀L1,T. L1 ≛[T] L2 → ❪G,L2❫ ⊢ ⬈*𝐒[h] T → ❪G,L1❫ ⊢ ⬈*𝐒[h] T.