-lemma drop_inv_skip2: â\88\80d,e,I,L1,K2,V2. â\86\91[d, e] K2. ð\9d\95\93{I} V2 â\89¡ L1 → 0 < d →
- â\88\83â\88\83K1,V1. â\86\91[d - 1, e] K2 â\89¡ K1 & ↑[d - 1, e] V2 ≡ V1 &
+lemma drop_inv_skip2: â\88\80d,e,I,L1,K2,V2. â\86\93[d, e] L1 â\89¡ K2. ð\9d\95\93{I} V2 → 0 < d →
+ â\88\83â\88\83K1,V1. â\86\93[d - 1, e] K1 â\89¡ K2 & ↑[d - 1, e] V2 ≡ V1 &