-definition CP3 ≝ λRP:lenv→predicate term.
- ∀L,V,k. RP L (ⓐ⋆k.V) → RP L V.
+definition CP3 ≝ λRP:relation3 genv lenv term.
+ ∀G,L,T,k. RP G L (ⓐ⋆k.T) → RP G L T.
+
+definition CP4 ≝ λRP:relation3 genv lenv term.
+ ∀G,L,W,T. RP G L W → RP G L T → RP G L (ⓝW.T).