proposition: Lemma acreate_fi (a b:Set) (f:a->b): injectiveC f -> injection (acreate f).
proof: Proof. move=> fi; split; first by fprops. move=> x y; rewrite {1 2} /acreate; aw => xa ya. rewrite -(B_eq xa) - (B_eq ya) (acreate_V f (Bo xa)) (acreate_V f (Bo ya)). by move=> eq; move: (R_inj eq)=> eqv; rewrite (fi _ _ eqv). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)