proposition: Lemma big_sumType (I1 I2 : finType) (P : pred (I1 + I2)) F : \big[*%M/1]_(i | P i) F i = (\big[*%M/1]_(i | P (inl _ i)) F (inl _ i)) * (\big[*%M/1]_(i | P (inr _ i)) F (inr _ i)).
proof: Proof. by rewrite ![index_enum _]unlock [@Finite.enum in LHS]unlock/= big_cat !big_map. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)