proposition: Lemma setU1_V_out f x y: fgraph f -> ~ (inc x (domain f)) -> Vg (f +s1 (J x y)) x = y.
proof: Proof. move=>ff /(fgraph_setU1 y ff) fg. have h1: inc (J x y) (f +s1 (J x y)) by fprops. by move: (pr2_V fg h1); aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)