fact: Fixpoint number_of_occurrences (a : A) (l : list A) {struct l} : nat := match l with | [] => 0 | b :: l1 => match A_eq_dec a b with | left _ => S (number_of_occurrences a l1) | right _ => number_of_occurrences a l1 end end.
imports: Coq(List Sorting.Permutation) Huffman(AuxLib UniqueKey)