proposition: Theorem cprod_An f g: partition_w_fam g (domain f) -> cprod f = cprodb (domain g) (fun l => cprodb (Vg g l) (Vg f)).
proof: Proof. move=> pfa. transitivity (cprodb (domain g) (fun l => restriction_product f (Vg g l))). apply/card_eqP. by exists (prod_assoc_map f g); split; first (by apply: pam_fb); rewrite/ prod_assoc_map; aw. apply: Eqc_setXb => //; split; aww. by move=> i idg; rewrite /cprodb /cprod /restriction_product !LgV //; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)