proposition: Lemma setU1_restr f x E: fgraph f -> ~ (inc x E) -> domain f = E +s1 x-> (restr f E) +s1 (J x (Vg f x)) = f.
proof: Proof. move=> fgf nxE df. have sEd: sub E (domain f) by rewrite df; fprops. have dr: (domain (restr f E)) = E by rewrite restr_d. have fgr: fgraph (restr f E) by fprops. have nxe: ~ inc x (domain (restr f E)) by ue. apply: fgraph_exten =>//. by apply: fgraph_setU1. by rewrite domain_setU1 dr df. move=> u; rewrite domain_setU1 dr; case/setU1_P => uE. have ud: inc u (domain (restr f E)) by rewrite dr. by rewrite setU1_V_in // restr_ev. by rewrite uE setU1_V_out. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)