proposition: Theorem in_frequency_map_inv : forall l a, In a (map (fst (B:=_)) (frequency_list l)) -> In a l.
proof: Proof. intros l a H; case (proj1 (in_map_iff _ _ _)) with (1 := H); auto. intros (a1, l1) (Hl2, Hl1); simpl in |- *. rewrite <- Hl2; apply frequency_list_in with (1 := Hl1). Qed.
imports: Coq(List Sorting.Permutation) Huffman(AuxLib UniqueKey)