-lemma lsx_lref_be_lpxs: ∀h,g,I,G,K1,V,i,l. l ≤ yinj i → ⦃G, K1⦄ ⊢ ⬊*[h, g] V →
- ∀K2. G ⊢ ⬊*[h, g, V, 0] K2 → ⦃G, K1⦄ ⊢ ➡*[h, g] K2 →
- ∀L2. ⬇[i] L2 ≡ K2.ⓑ{I}V → G ⊢ ⬊*[h, g, #i, l] L2.
-#h #g #I #G #K1 #V #i #l #Hli #H @(csx_ind_alt … H) -V
+lemma lsx_lref_be_lpxs: ∀h,o,I,G,K1,V,i,l. l ≤ yinj i → ⦃G, K1⦄ ⊢ ⬊*[h, o] V →
+ ∀K2. G ⊢ ⬊*[h, o, V, 0] K2 → ⦃G, K1⦄ ⊢ ➡*[h, o] K2 →
+ ∀L2. ⬇[i] L2 ≡ K2.ⓑ{I}V → G ⊢ ⬊*[h, o, #i, l] L2.
+#h #o #I #G #K1 #V #i #l #Hli #H @(csx_ind_alt … H) -V