lemma ldrop_fwd_be: ∀L,K,s,d,e,i. ⇩[s, d, e] L ≡ K → |K| ≤ i → i < d → |L| ≤ i.
#L #K #s #d #e #i #HLK #HK #Hd elim (lt_or_ge i (|L|)) //
lemma ldrop_fwd_be: ∀L,K,s,d,e,i. ⇩[s, d, e] L ≡ K → |K| ≤ i → i < d → |L| ≤ i.
#L #K #s #d #e #i #HLK #HK #Hd elim (lt_or_ge i (|L|)) //