-lemma csx_lpxs_conf: ∀h,G,L1,L2,T. ⦃G,L1⦄ ⊢ ⬈*[h] L2 →
- ⦃G,L1⦄ ⊢ ⬈*[h] 𝐒⦃T⦄ → ⦃G,L2⦄ ⊢ ⬈*[h] 𝐒⦃T⦄.
-#h #G #L1 #L2 #T #H @(lpxs_ind_dx … H) -L2
+lemma csx_lpxs_conf (G) (L1):
+ ∀L2,T. ❪G,L1❫ ⊢ ⬈* L2 → ❪G,L1❫ ⊢ ⬈*𝐒 T → ❪G,L2❫ ⊢ ⬈*𝐒 T.
+#G #L1 #L2 #T #H @(lpxs_ind_dx … H) -L2