proposition: Lemma nuBy_nodup {A} (eq : A -> A -> bool) (l : list A) : (forall x y, (eq x y = true) <-> (x = y)) -> NoDup (nubBy eq l).
proof: Proof. funelim (nubBy eq l). constructor. intros Heq; specialize (H Heq). constructor. intros Hi. apply In_nubBy, In_filter in Hi as [_ eqaa]. specialize (Heq x x). destruct (eq x x). discriminate. destruct (proj2 Heq). reflexivity. discriminate. auto. Qed.
imports: Equations(Equations) Coq(List Program.Syntax Arith Lia) List