-lemma cprs_delta: ∀L,K,V,V2,i.
- ⇩[0, i] L ≡ K. ⓓV → K ⊢ V ➡* V2 →
- ∀W2. ⇧[0, i + 1] V2 ≡ W2 → L ⊢ #i ➡* W2.
-#L #K #V #V2 #i #HLK #H elim H -V2 [ /3 width=6/ ]
+lemma cprs_delta: ∀G,L,K,V,V2,i.
+ ⇩[0, i] L ≡ K.ⓓV → ⦃G, K⦄ ⊢ V ➡* V2 →
+ ∀W2. ⇧[0, i + 1] V2 ≡ W2 → ⦃G, L⦄ ⊢ #i ➡* W2.
+#G #L #K #V #V2 #i #HLK #H elim H -V2 [ /3 width=6/ ]