-lemma drop_leq_drop1: ∀L1,L2,d,e. L1 [d, e] ≈ L2 →
- ∀I,K1,V,i. ↓[0, i] L1 ≡ K1. 𝕓{I} V →
- d ≤ i → i < d + e →
- ∃∃K2. K1 [0, d + e - i - 1] ≈ K2 &
- ↓[0, i] L2 ≡ K2. 𝕓{I} V.
+lemma drop_lsubs_drop1_abbr: ∀L1,L2,d,e. L1 [d, e] ≼ L2 →
+ ∀K1,V,i. ↓[0, i] L1 ≡ K1. 𝕓{Abbr} V →
+ d ≤ i → i < d + e →
+ ∃∃K2. K1 [0, d + e - i - 1] ≼ K2 &
+ ↓[0, i] L2 ≡ K2. 𝕓{Abbr} V.