proposition: Lemma countMapZero (X Y: eqType) (x x':X) (B: list Y) y : x' <> x -> count ( map (fun y => (x,y)) B) (x', y) =0.
proof: Proof. intros ineq. induction B. - reflexivity. - simpl. dec. + inversion e; congruence. + exact IHB. Qed.
imports: Undecidability.Shared.Libs.PSL(FinTypesDef)