proposition: Lemma NoDup_fmap_fst {A B} (l : list (A * B)) : (∀ x y1 y2, (x,y1) ∈ l → (x,y2) ∈ l → y1 = y2) → NoDup l → NoDup (l.*1).
proof: Proof. intros Hunique. induction 1 as [|[x1 y1] l Hin Hnodup IH]; csimpl; constructor. - rewrite elem_of_list_fmap. intros [[x2 y2] [??]]; simpl in *; subst. destruct Hin. rewrite (Hunique x2 y1 y2); rewrite ?elem_of_cons; auto. - apply IH. intros. eapply Hunique; rewrite ?elem_of_cons; eauto. Qed.
imports: stdpp(options)