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