proposition: Lemma nubBy_length {A} (eq : A -> A -> bool) (l : list A) : length (nubBy eq l) <= length l.
proof: Proof. funelim (nubBy eq l); simpl; trivial. rewrite filter_length in H. auto with arith. Qed.
imports: Equations(Equations) Coq(List Program.Syntax Arith Lia) List