proposition: Lemma count_count_occ {X : Type} {HX : eq_dec X} (l : list X) x : count l x = count_occ HX l x.
proof: Proof. induction l as [|y l IH]; [easy|]. cbn. rewrite IH. unfold Dec. now destruct (HX x y); destruct (HX y x); congruence. Qed.
imports: Undecidability.Shared.Libs.PSL(FinTypesDef)