proposition: Lemma countMap_zero (X Y : eqType) (A : list X) (y : Y) (f : X -> Y) : (forall x, f x <> y) -> FinTypesDef.count (map f A) y = 0.
proof: Proof. revert y. induction A as [ | a A IH]; intros; cbn in *; auto. decide (y = f a) as [-> | ?]; auto. now contradiction (H a). Qed.
imports: Undecidability(TM.Util.Prelim) Coq.Lists.List