proposition: Lemma prod_assoc_map2 f g: prod_assoc_axioms f g -> domain g = C2 -> (productb f) \Eq ((restriction_product f(Vg g C0)) \times (restriction_product f (Vg g C1))).
proof: Proof. move=> pam dg. set h := (productf (domain g) (fun l => (restriction_product f (Vg g l)))). have ea: productb f \Eq h. exists (prod_assoc_map f g). by split; first (by apply: pam_fb); rewrite /prod_assoc_map; aw. apply: (EqT ea); apply:EqS. exists (product2_canon (restriction_product f (Vg g C0)) (restriction_product f (Vg g C1))). rewrite /bijection_prop/product2_canon; aw; split => //. by apply: product2_canon_fb. rewrite /h dg; congr (productb _); apply: Lg_exten. move=> x xt; try_lvariant xt; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)