YES ---- CR(R) ---- R : linear and strongly closed [Huet, 1980] R: F(c(x)) -> G(x) G(x) -> F(x) c(x) -> x CP(R): F(___y13) -> G(___y13)