proposition: Lemma big_unitType (P : pred unit) (F : unit -> X) : \big[*%M/1]_(x | P x) F x ≡ if P tt then F tt else 1.
proof: Proof. by rewrite ![index_enum _]unlock [@Finite.enum]unlock big_mkcond big_seq1. Qed.
imports: HB(structures) Coq(RelationClasses Morphisms Relation_Definitions) mathcomp(all_ssreflect)