proposition: Lemma pre_rel_func R P : functional R -> functional (pre_rel P R).
proof: Proof. by move=> funcR x y1 y2 [_ Rxy1] [_ /(funcR _ _ _ Rxy1)]. Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)