proposition: Lemma restr_to_domain f g: fgraph f -> sub g f -> restr f (domain g) = g.
proof: Proof. move => h1 h2; move: (sub_fgraph h1 h2) => fgg. apply:fgraph_exten; aw; fprops. by move => t tx; rewrite (LgV tx); symmetry; apply: sub_graph_ev. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)