theorem drop_trans_le: ∀L1,L,s1,l1,m1. ⬇[s1, l1, m1] L1 ≡ L →
∀L2,s2,m2. ⬇[s2, 0, m2] L ≡ L2 → m2 ≤ l1 →
∃∃L0. ⬇[s2, 0, m2] L1 ≡ L0 & ⬇[s1, l1 - m2, m1] L0 ≡ L2.
theorem drop_trans_le: ∀L1,L,s1,l1,m1. ⬇[s1, l1, m1] L1 ≡ L →
∀L2,s2,m2. ⬇[s2, 0, m2] L ≡ L2 → m2 ≤ l1 →
∃∃L0. ⬇[s2, 0, m2] L1 ≡ L0 & ⬇[s1, l1 - m2, m1] L0 ≡ L2.