proposition: Lemma fpf_V f x y: inc f fBCA -> inc x B -> inc y C -> Vf (first_partial_fun f y) x = Vf f (J x y).
proof: Proof. rewrite/first_partial_fun=> pfa xd yr. by rewrite LfV //; apply: fpf_axiom. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)