proposition: Lemma ext_to_prod_V a b: inc a (source u) -> inc b (source v)-> Vf (u \ftimes v) (J a b) = J (Vf u a) (Vf v b).
proof: Proof. by move => asu bsv; rewrite ext_to_prod_V2; aw; trivial; apply: setXp_i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)