-lemma lsx_ge_up: ∀h,g,G,L,T,U,dt,d,e. dt ≤ yinj d + yinj e →
- â\87§[d, e] T â\89¡ U â\86\92 G â\8a¢ â\8b\95â¬\8a*[h, g, U, dt] L â\86\92 G â\8a¢ â\8b\95â¬\8a*[h, g, U, d] L.
-#h #g #G #L #T #U #dt #d #e #Hdtde #HTU #H @(lsx_ind … H) -L
+lemma lsx_ge_up: ∀h,o,G,L,T,U,lt,l,k. lt ≤ yinj l + yinj k →
+ â¬\86[l, k] T â\89¡ U â\86\92 G â\8a¢ â¬\8a*[h, o, U, lt] L â\86\92 G â\8a¢ â¬\8a*[h, o, U, l] L.
+#h #o #G #L #T #U #lt #l #k #Hltlm #HTU #H @(lsx_ind … H) -L