proposition: Lemma ProdCount (T1 T2: eqType) (A: list T1) (B: list T2) (a:T1) (b:T2) : count (list_prod A B) (a,b) = count A a * count B b .
proof: Proof. induction A. - reflexivity. - cbn. rewrite <- countSplit. decide (a = a0) as [E | E]. + cbn. f_equal. subst a0. apply countMap. eauto. + rewrite <- plus_O_n. f_equal. now apply countMapZero. eauto. Qed.
imports: Undecidability.Shared.Libs.PSL(FinTypes)