proposition: Lemma bcreate_inv1 f (H:function f): acreate (bcreate1 H) = f.
proof: Proof. apply: function_exten; fprops; rewrite {1}/acreate; aw; trivial. by move=> x xs; rewrite - (B_eq xs) acreate_V; apply: prop_bcreate1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)