-definition CP2 ≝ λRR:lenv→relation term. λRS:relation term.
- ∀L,K,W,i. ⇩[0,i] L ≡ K. ⓛW → NF … (RR L) RS (#i).
+definition CP2 ≝ λRR:relation4 genv lenv term term. λRS:relation term.
+ ∀G,L0,L,T,T0,d,e. NF … (RR G L) RS T →
+ ⇩[d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → NF … (RR G L0) RS T0.