proposition: Theorem NoDup_unique_key : forall l : list (A * B), NoDup (map (fst (B:=_)) l) -> unique_key l.
proof: Proof. intros l; elim l; simpl in |- *; auto. intros a; case a. intros a0 b l0 H H0; apply unique_key_cons; auto. intros b0; red in |- *; intros H1; absurd (In a0 (map (fst (B:=_)) l0)); auto. inversion H0; auto. change (In (fst (a0, b0)) (map (fst (B:=_)) l0)) in |- *; auto with datatypes. apply in_map; auto. apply H; apply NoDup_cons_iff with (1 := H0); auto. Qed.
imports: Coq(Sorting.Permutation)