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