qed.
lemma thin_ldrop_conf_be: ∀L0,L1,d1,e1. ▼*[d1, e1] L0 ≡ L1 →
∀L2,e2. ⇩[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
∃∃L. ▼*[0, d1 + e1 - e2] L2 ≡ L & ⇩[0, d1] L1 ≡ L.
#L0 #L1 #d1 #e1 * #L #HL0 #HL1 #L2 #e2 #HL02 #Hd1e2 #He2de1
qed.
lemma thin_ldrop_conf_be: ∀L0,L1,d1,e1. ▼*[d1, e1] L0 ≡ L1 →
∀L2,e2. ⇩[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
∃∃L. ▼*[0, d1 + e1 - e2] L2 ≡ L & ⇩[0, d1] L1 ≡ L.
#L0 #L1 #d1 #e1 * #L #HL0 #HL1 #L2 #e2 #HL02 #Hd1e2 #He2de1