proposition: Lemma dupfreeCount (X: eqType) (x:X) (A: list X) : NoDup A -> x el A -> count A x = 1.
proof: Proof. intros D E. induction D. - contradiction E. - cbn. dec. + f_equal. subst x0. now apply notInZero. + destruct E as [E | E]; [> congruence | auto]. Qed.
imports: Undecidability.Shared.Libs.PSL(FinTypesDef)