proposition: Lemma NoDup_list_difference l k : NoDup l → NoDup (list_difference l k).
proof: Proof. induction 1; simpl; try case_decide. - constructor. - done. - constructor; [|done]. rewrite elem_of_list_difference; intuition. Qed.
imports: stdpp(options)