proposition: Lemma acreate_exten (a b: Set) (f g: a-> b): f =1 g -> acreate f = acreate g.
proof: Proof. move=> h; apply: function_exten; aww. by move=> x [z za]; rewrite -za ! acreate_V h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)