fact ldrop_inv_skip2_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → 0 < d →
∀I,K2,V2. L2 = K2. 𝕓{I} V2 →
∃∃K1,V1. ↓[d - 1, e] K1 ≡ K2 &
↑[d - 1, e] V2 ≡ V1 &
L1 = K1. 𝕓{I} V1.
fact ldrop_inv_skip2_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → 0 < d →
∀I,K2,V2. L2 = K2. 𝕓{I} V2 →
∃∃K1,V1. ↓[d - 1, e] K1 ≡ K2 &
↑[d - 1, e] V2 ≡ V1 &
L1 = K1. 𝕓{I} V1.