proposition: Lemma countMap_injective (X Y : eqType) (x : X) (A : list X) (f : X -> Y) : (forall x y, f x = f y -> x = y) -> FinTypesDef.count (map f A) (f x) = FinTypesDef.count A x.
proof: Proof. intros HInj. revert x. induction A as [ | a A IH]; intros; cbn in *; auto. decide (f x = f a) as [ -> % HInj | He]. - decide (a = a) as [_ | Ha]; auto. congruence. - decide (x = a) as [-> | Hx]; auto. congruence. Qed.
imports: Undecidability(TM.Util.Prelim) Coq.Lists.List