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.
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.