-lemma csx_lpxs_conf: ∀h,o,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, o] L2 →
- ∀T. ⦃G, L1⦄ ⊢ ⬊*[h, o] T → ⦃G, L2⦄ ⊢ ⬊*[h, o] T.
-#h #o #G #L1 #L2 #H @(lpxs_ind … H) -L2 /3 by lpxs_strap1, csx_lpx_conf/
+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
+/3 by lpxs_step_dx, csx_lpx_conf/