proposition: Lemma countMap (X Y: eqType) (x:X) (B: list Y) y : count ( map (fun y => (x,y)) B) (x, y) = count B y.
proof: Proof. induction B. - reflexivity. - simpl. dec; congruence. Qed.
imports: Undecidability.Shared.Libs.PSL(FinTypesDef)