proposition: Lemma ext_map_prod_V x: inc x (productf I src) -> Vf (ext_map_prod I src trg f) x = Lg I (ext_map_prod_aux x f).
proof: Proof. move => h; rewrite LfV //; apply: ext_map_prod_taxioms. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)