-lemma lsx_inv_lift_be: ∀h,g,G,L,T,U,dt,d,e. yinj d ≤ dt → dt ≤ d + e →
- ⬆[d, e] T ≡ U → G ⊢ ⬊*[h, g, U, dt] L →
- ∀K. ⬇[Ⓕ, d, e] L ≡ K → G ⊢ ⬊*[h, g, T, d] K.
-#h #g #G #L #T #U #dt #d #e #Hddt #Hdtde #HTU #H @(lsx_ind … H) -L
+lemma lsx_inv_lift_be: ∀h,g,G,L,T,U,lt,l,m. yinj l ≤ lt → lt ≤ l + m →
+ ⬆[l, m] T ≡ U → G ⊢ ⬊*[h, g, U, lt] L →
+ ∀K. ⬇[Ⓕ, l, m] L ≡ K → G ⊢ ⬊*[h, g, T, l] K.
+#h #g #G #L #T #U #lt #l #m #Hllt #Hltlm #HTU #H @(lsx_ind … H) -L