proposition: Lemma NoDup_fmap_2_strong l : (∀ x y, x ∈ l → y ∈ l → f x = f y → x = y) → NoDup l → NoDup (f <$> l).
proof: Proof. intros Hinj. induction 1 as [|x l ?? IH]; simpl; constructor. - intros [y [Hxy ?]]%elem_of_list_fmap. apply Hinj in Hxy; [by subst|by constructor..]. - apply IH. clear- Hinj. intros x' y Hx' Hy. apply Hinj; by constructor. Qed.
imports: stdpp(options)