proposition: Lemma sub_graph_ev f g: fgraph g -> sub f g -> {inc (domain f), f =1g g}.
proof: Proof. move=> fg sfg x xdf. set ipg:=(sfg _ (fdomain_pr1 (sub_fgraph fg sfg) xdf)). by move: (in_graph_V fg ipg); aw; apply: pr2_def. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)