-lemma lsx_ge_up: ∀h,g,G,L,T,U,lt,l,m. lt ≤ yinj l + yinj m →
- ⬆[l, m] T ≡ U → G ⊢ ⬊*[h, g, U, lt] L → G ⊢ ⬊*[h, g, U, l] L.
-#h #g #G #L #T #U #lt #l #m #Hltlm #HTU #H @(lsx_ind … H) -L
+lemma lsx_ge_up: ∀h,o,G,L,T,U,lt,l,k. lt ≤ yinj l + yinj k →
+ ⬆[l, k] T ≡ U → G ⊢ ⬊*[h, o, U, lt] L → G ⊢ ⬊*[h, o, U, l] L.
+#h #o #G #L #T #U #lt #l #k #Hltlm #HTU #H @(lsx_ind … H) -L