∀L2,e2. ⇩[0, e2] L0 ≡ L2 →
d1 ≤ e2 → ⇩[0, e1 + e2] L1 ≡ L2.
#L1 #L0 #d1 #e1 * #L #HL1 #HL0 #L2 #e2 #HL02 #Hd1e2
lapply (ldrop_trans_ge … HL0 … HL02 ?) -L0 // #HL2
∀L2,e2. ⇩[0, e2] L0 ≡ L2 →
d1 ≤ e2 → ⇩[0, e1 + e2] L1 ≡ L2.
#L1 #L0 #d1 #e1 * #L #HL1 #HL0 #L2 #e2 #HL02 #Hd1e2
lapply (ldrop_trans_ge … HL0 … HL02 ?) -L0 // #HL2