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