theorem drop_trans_le: ∀d1,e1,L1,L. ↓[d1, e1] L1 ≡ L →
∀e2,L2. ↓[0, e2] L ≡ L2 → e2 ≤ d1 →
∃∃L0. ↓[0, e2] L1 ≡ L0 & ↓[d1 - e2, e1] L0 ≡ L2.
theorem drop_trans_le: ∀d1,e1,L1,L. ↓[d1, e1] L1 ≡ L →
∀e2,L2. ↓[0, e2] L ≡ L2 → e2 ≤ d1 →
∃∃L0. ↓[0, e2] L1 ≡ L0 & ↓[d1 - e2, e1] L0 ≡ L2.