proposition: Lemma fpfb_VV f x: inc f fBCA -> inc x (B \times C) -> Vf (Vf (Vf (first_partial_map) f) (Q x)) (P x) = Vf f x.
proof: Proof. move=> fs xp; rewrite fpfb_V=>//. move /setX_P: xp =>[xp px qx]. by rewrite fpfa_V // fpf_V // xp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)