proposition: Lemma NoDup_list_union l k : NoDup l → NoDup k → NoDup (list_union l k).
proof: Proof. intros. apply NoDup_app. repeat split. - by apply NoDup_list_difference. - intro. rewrite elem_of_list_difference. intuition. - done. Qed.
imports: stdpp(options)