proposition: Lemma In_nubBy {A} (eq : A -> A -> bool) (l : list A) (a : A) : In a (nubBy eq l) -> In a l.
proof: Proof. funelim (nubBy eq l). + trivial. + intros H0. destruct H0 as [->|H0]; auto. simpl. auto. specialize (H _ H0). apply In_filter in H as [Inal eqa]. right; auto. Qed.
imports: Equations(Equations) Coq(List Program.Syntax Arith Lia) List