proposition: Lemma acreate_function (A B:Set) (f:A->B): function (acreate f).
proof: Proof. move: (acreate_triple f)=>cf; split=> //. split; fprops; move=> x y /acreate_P [v1 ->]/acreate_P [v2 ->]; aw=> eql. by rewrite (R_inj eql). rewrite /acreate /gacreate /domain; aw. set_extens t. move=> tA; apply/funI_P;exists (J t (Ro (f (Bo tA)))); last by aw. by apply /IM_P; exists (Bo tA); rewrite B_eq. move/funI_P => [x /IM_P [a ->] ->]; aw; trivial; apply: R_inc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)