proposition: Lemma Eq_domain f: fgraph f -> domain f \Eq f.
proof: Proof. move => h. apply:(@equipotent_aux (fun z => J z (Vg f z))); apply: lf_bijective. + by apply: fdomain_pr1. + by move => u v _ _ /pr1_def. + by move => y yf; rewrite (in_graph_V h yf); exists (P y); fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)