proposition: Lemma bcreate_inv3 (A B:Set) (f:A->B): bcreate (acreate_function f) (acreate_source f)(acreate_target f) =1 f.
proof: Proof. by move=> a;apply: R_inj; rewrite prop_bcreate2 acreate_V. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)