proposition: Lemma acreate_P (A B:Set) (f:A->B) x: inc x (graph (acreate f)) <-> exists u:A, x = J (Ro u) (Ro (f u)).
proof: Proof. rewrite /acreate /gacreate; aw; apply/IM_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)