proposition: Lemma fgraph_exten f g: fgraph f -> fgraph g -> domain f = domain g -> {inc (domain f), f =1g g} -> f = g.
proof: Proof. move=> ff fg sd hyp; set_extens t => tf. have pa:= (domain_i1 tf). rewrite (in_graph_V ff tf) (hyp _ pa); apply: fdomain_pr1 => //; ue. move: (domain_i1 tf); rewrite - sd => pa. by rewrite (in_graph_V fg tf) - (hyp _ pa); apply: fdomain_pr1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)