proposition: Lemma fpfa_V f y: inc f fBCA -> inc y C -> Vf (first_partial_function f) y = first_partial_fun f y.
proof: Proof. rewrite /first_partial_function=> pfa yr. by rewrite LfV //; apply: fpfa_axiom. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)