proposition: Theorem frequency_list_unique : forall l : list A, unique_key (frequency_list l).
proof: Proof. intros l; elim l; simpl in |- *; auto. intros a l0 H; apply add_frequency_list_unique_key; auto. Qed.
imports: Coq(List Sorting.Permutation) Huffman(AuxLib UniqueKey)