proposition: Lemma in_graph_V x: inc x f -> x = J (P x) (Vg f (P x)).
proof: Proof. move => xf; apply: (proj2 fgf _ _ xf); aww. by apply:fdomain_pr1=> //; apply: domain_i1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)