proposition: Lemma iim_fun_C g x: function g -> Vfi g ((target g) -s x) = (source g) -s (Vfi g x).
proof: Proof. move => fg. have gg: sgraph (graph g) by fprops. set_extens t. move/iim_graph_P => [u /setC_P [ut nux] Jug];apply/setC_P. split; first by Wtac. move/iim_graph_P => [w wx Jwg]. by case: nux; rewrite (fgraph_pr (proj32 fg) Jug Jwg). move/setC_P => [ts neu]. have Jg: (inc (J t (Vf g t))(graph g)) by Wtac. apply/iim_graph_P; ex_tac;apply/setC_P; split; fprops. dneg Wx; apply/iim_graph_P; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)