-lemma lsx_flat_lpxs: ∀h,g,I,G,L1,V,d. G ⊢ ⬊*[h, g, V, d] L1 →
- ∀L2,T. G ⊢ ⬊*[h, g, T, d] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2 →
- G ⊢ ⬊*[h, g, ⓕ{I}V.T, d] L2.
-#h #g #I #G #L1 #V #d #H @(lsx_ind_alt … H) -L1
+lemma lsx_flat_lpxs: ∀h,g,I,G,L1,V,l. G ⊢ ⬊*[h, g, V, l] L1 →
+ ∀L2,T. G ⊢ ⬊*[h, g, T, l] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2 →
+ G ⊢ ⬊*[h, g, ⓕ{I}V.T, l] L2.
+#h #g #I #G #L1 #V #l #H @(lsx_ind_alt … H) -L1