+definition CP4 ≝ λ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 CP4s ≝ λRR:lenv→relation term. λRS:relation term.
+ ∀L0,L,des. ⇓[des] L0 ≡ L →
+ ∀T,T0. ⇑[des] T ≡ T0 →
+ NF … (RR L) RS T → NF … (RR L0) RS T0.
+