fact: Definition huffman_aux : forall l : list (nat * code A), huffman_aux_type l := list_length_induction (nat * code A) huffman_aux_type huffman_aux_F.
imports: Coq(Sorting.Permutation) Huffman(Code BTree Build PBTree2BTree Restrict)