-lemma drops_inv_skip2: ∀I,s,des,des2,i. des ▭ i ≡ des2 →
- ∀L1,K2,V2. ⬇*[s, des2] L1 ≡ K2. ⓑ{I} V2 →
- ∃∃K1,V1,des1. des + 1 ▭ i + 1 ≡ des1 + 1 &
- ⬇*[s, des1] K1 ≡ K2 &
- ⬆*[des1] V2 ≡ V1 &
+lemma drops_inv_skip2: ∀I,s,cs,cs2,i. cs ▭ i ≡ cs2 →
+ ∀L1,K2,V2. ⬇*[s, cs2] L1 ≡ K2. ⓑ{I} V2 →
+ ∃∃K1,V1,cs1. cs + 1 ▭ i + 1 ≡ cs1 + 1 &
+ ⬇*[s, cs1] K1 ≡ K2 &
+ ⬆*[cs1] V2 ≡ V1 &