proposition: Lemma pam_V f g x: prod_assoc_axioms f g -> inc x (productb f) -> Vf (prod_assoc_map f g) x = (Lg (domain g) (fun l => Vf (pr_j f (Vg g l)) x)).
proof: Proof. by move => ax xp; rewrite LfV //; apply: pam_axiom. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)