proposition: Lemma set_inter_nodup l l' : NoDup l -> NoDup l' -> NoDup (set_inter l l').
proof: Proof. induction 1 as [|x l H H' IH]; intro Hl'; simpl. - constructor. - destruct (set_mem x l'); auto. constructor; auto. rewrite set_inter_iff; tauto. Qed.
imports: List