proposition: Lemma partial_fun2_V x y: inc (J x y) (source f) -> Vf (partial_fun2 f y) x = Vf f (J x y).
proof: Proof. move=> Js; apply: LfV => //; first by apply: partial_fun2_axioms. apply /iim_graph_P; ex_tac; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)