-definition CP2 ≝ λRR:lenv→relation term. λRS:relation term.
- ∀L0,L,T,T0,d,e. NF … (RR L) RS T →
- ⇩[d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → NF … (RR L0) RS T0.
+definition CP2 ≝ λ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.