proposition: Lemma restriction_graph2 f J: fgraph f -> sub J (domain f) -> Lg J (Vg f) = f \cg (diagonal J).
proof: Proof. move=> fgj sj. rewrite diagonal_is_identity - compg_composef. by rewrite/composef identity_d; apply: Lg_exten => i idx; rewrite identity_ev. hnf;rewrite identity_r;split => //; apply: identity_fgraph. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)