proposition: Theorem frequency_list_perm : forall l : list A, Permutation l (flat_map (fun p => id_list (fst p) (snd p)) (frequency_list l)).
proof: Proof. intros l; elim l; simpl in |- *; auto. intros a l0 H. apply Permutation_trans with (2 := add_frequency_list_perm a (frequency_list l0)); auto. Qed.
imports: Coq(List Sorting.Permutation) Huffman(AuxLib UniqueKey)