proposition: Lemma NoDup_bind l : (∀ x1 x2 y, x1 ∈ l → x2 ∈ l → y ∈ f x1 → y ∈ f x2 → x1 = x2) → (∀ x, x ∈ l → NoDup (f x)) → NoDup l → NoDup (l ≫= f).
proof: Proof. intros Hinj Hf. induction 1 as [|x l ?? IH]; csimpl; [constructor|]. apply NoDup_app. split_and!. - eauto 10 using elem_of_list_here. - intros y ? (x'&?&?)%elem_of_list_bind. destruct (Hinj x x' y); auto using elem_of_list_here, elem_of_list_further. - eauto 10 using elem_of_list_further. Qed.
imports: stdpp(options)