proposition: Lemma fgraph_bd x A: fgraph x -> natp (domain x) -> (forall i, inc i (domain x) -> inc (Vg x i) A) -> inc x (\Po (Nat \times A)).
proof: Proof. move => fgx dx vx; apply/setP_P => t tx. move: (domain_i1 tx) => tdx. rewrite (in_graph_V fgx tx); exact:(setXp_i (NS_inc_nat dx tdx) (vx _ tdx)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)