proposition: Lemma acreate_V (A B:Set) (f:A->B) (x:A): Vf (acreate f) (Ro x) = Ro (f x).
proof: Proof. have rs: (inc (Ro x) (source (acreate f))) by rewrite/acreate; aw; apply: R_inc. move: (Vf_pr3 (acreate_function f) rs) => /acreate_P [u eql]. by rewrite (pr2_def eql) (R_inj (pr1_def eql)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)