proposition: Lemma NoDupA_unique_repr (l:list key) x y : NoDupA K.eq l -> K.eq x y -> List.In x l -> List.In y l -> x = y.
proof: Proof. intros H E Hx Hy. induction H; simpl in *. - inversion Hx. - intuition; subst; trivial. elim H. apply InA_alt. now exists y. elim H. apply InA_alt. now exists x. Qed.
imports: Coq(EqualitiesFacts)