proposition: Lemma bcreate_inv2 f A B (H:function f) (Ha:source f = A)(Hb:target f = B): acreate (bcreate H Ha Hb) = f.
proof: Proof. apply: function_exten; fprops; rewrite /acreate; aw =>//. by move=> x xs; rewrite -(B_eq xs) acreate_V; apply: prop_bcreate2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)