-lemma cpg_delta_drops: ∀Rt,c,h,G,K,V,V2,i,L,T2. ⬇*[i] L ≘ K.ⓓV → ⦃G, K⦄ ⊢ V ⬈[Rt, c, h] V2 →
- ⬆*[↑i] V2 ≘ T2 → ⦃G, L⦄ ⊢ #i ⬈[Rt, c, h] T2.
+lemma cpg_delta_drops: ∀Rt,c,h,G,K,V,V2,i,L,T2. ⬇*[i] L ≘ K.ⓓV → ⦃G,K⦄ ⊢ V ⬈[Rt,c,h] V2 →
+ ⬆*[↑i] V2 ≘ T2 → ⦃G,L⦄ ⊢ #i ⬈[Rt,c,h] T2.