proposition: Lemma spfa_V f x: inc f fBCA -> inc x B -> Vf (second_partial_function f) x = second_partial_fun f x.
proof: Proof. rewrite /second_partial_function=> pfa yr. by rewrite LfV //; apply: spfa_axiom. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)