proposition: Theorem all_pbleaves_pbleaf : forall l a1 a2, all_pbleaves (pbadd a1 (pbleaf a2) l) = a1 :: [].
proof: Proof. intros l; elim l; simpl in |- *; auto. intros b; case b; simpl in |- *; auto. Qed.
imports: Coq(List Compare_dec Sorting.Permutation) Huffman(AuxLib Code Build ISort UniqueKey)