proposition: Lemma prj_VV x i: inc x (productb f) -> inc i J -> Vg (Vf (pr_j f J) x) i = Vg x i.
proof: Proof. move=> xp ij; rewrite prj_V //. by move /setXb_P: xp => [fw dd _]; rewrite LgV //; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)