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