-lemma cpxs_delta_drops: ∀h,I,G,L,K,V1,V2,i.
- ⬇*[i] L ≘ K.ⓑ{I}V1 → ⦃G, K⦄ ⊢ V1 ⬈*[h] V2 →
- ∀W2. ⬆*[⫯i] V2 ≘ W2 → ⦃G, L⦄ ⊢ #i ⬈*[h] W2.
-#h #I #G #L #K #V1 #V2 #i #HLK #H @(cpxs_ind … H) -V2
+lemma cpxs_delta_drops (G) (L):
+ ∀I,K,V1,V2,i. ⇩[i] L ≘ K.ⓑ[I]V1 → ❪G,K❫ ⊢ V1 ⬈* V2 →
+ ∀W2. ⇧[↑i] V2 ≘ W2 → ❪G,L❫ ⊢ #i ⬈* W2.
+#G #L #I #K #V1 #V2 #i #HLK #H @(cpxs_ind … H) -V2