proposition: Lemma mapfst_ok {elt}(m:t elt) : NoDupA K.eq (List.map fst m) <-> NoDupA eqk m.
proof: Proof. induction m as [| (k,e) m IH]; simpl. - split; constructor. - split; inversion_clear 1; constructor; try apply IH; trivial. + contradict H0. rewrite mapfst_InA. eapply In_alt'; eauto. + rewrite mapfst_InA. contradict H0. now apply In_alt'. Qed.
imports: Coq(EqualitiesFacts)