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