-definition CP1 ≝ λRR:lenv→relation term. λRS:relation term.
- ∀L,k. NF … (RR L) RS (⋆k).
+definition CP0 ≝ λRR:relation4 genv lenv term term. λRS:relation term.
+ ∀G,L0,L,T,T0,s,d,e. NF … (RR G L) RS T →
+ ⇩[s, d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → NF … (RR G L0) RS T0.