proposition: Lemma pam_fi f g: prod_assoc_axioms f g -> injection (prod_assoc_map f g).
proof: Proof. move=> pa; split; first by apply: pam_f. have sp:(source (prod_assoc_map f g) = productb f). by rewrite /prod_assoc_map; aw. rewrite sp {sp} => x y xs ys. rewrite (pam_V pa xs)(pam_V pa ys) => sv. move: pa=> [fg md ugdf]. apply: (@setXb_exten _ x y xs ys) => i; rewrite - ugdf. move/setUb_P => [z zd iV]. have svf: sub (Vg g z) (domain f) by move=> t tv; rewrite - ugdf; union_tac. move:(congr1 (Vg ^~ z) sv); rewrite !LgV // !prj_V // => /(congr1 (Vg ^~i)). rewrite !LgV //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)