-lemma cpm_delta_drops: ∀n,h,G,L,K,V,V2,W2,i.
- ⇩[i] L ≘ K.ⓓV → ❪G,K❫ ⊢ V ➡[n,h] V2 →
- ⇧[↑i] V2 ≘ W2 → ❪G,L❫ ⊢ #i ➡[n,h] W2.
-#n #h #G #L #K #V #V2 #W2 #i #HLK *
+lemma cpm_delta_drops: ∀h,n,G,L,K,V,V2,W2,i.
+ ⇩[i] L ≘ K.ⓓV → ❪G,K❫ ⊢ V ➡[h,n] V2 →
+ ⇧[↑i] V2 ≘ W2 → ❪G,L❫ ⊢ #i ➡[h,n] W2.
+#h #n #G #L #K #V #V2 #W2 #i #HLK *