-lemma lsuby_ldrop_trans_be: ∀L1,L2,d,e. L1 ⊆[d, e] L2 →
- ∀I2,K2,W,s,i. ⇩[s, 0, i] L2 ≡ K2.ⓑ{I2}W →
- d ≤ i → i < d + e →
- ∃∃I1,K1. K1 ⊆[0, ⫰(d+e-i)] K2 & ⇩[s, 0, i] L1 ≡ K1.ⓑ{I1}W.
+lemma lsuby_drop_trans_be: ∀L1,L2,d,e. L1 ⊆[d, e] L2 →
+ ∀I2,K2,W,s,i. ⬇[s, 0, i] L2 ≡ K2.ⓑ{I2}W →
+ d ≤ i → i < d + e →
+ ∃∃I1,K1. K1 ⊆[0, ⫰(d+e-i)] K2 & ⬇[s, 0, i] L1 ≡ K1.ⓑ{I1}W.