proposition: Lemma big_sumType (I1 I2 : finType) (P : pred (I1 + I2)) (F : (I1 + I2) -> X) : \big[*%M/1]_(x | P x) F x ≡ (\big[*%M/1]_(x | P (inl x)) F (inl x)) ⊗ (\big[*%M/1]_(x | P (inr x)) F (inr x)).
proof: Proof. by rewrite ![index_enum _]unlock [@Finite.enum in X in X ≡ _]unlock big_cat !big_map. Qed.
imports: HB(structures) Coq(RelationClasses Morphisms Relation_Definitions) mathcomp(all_ssreflect)