proposition: Theorem distinct_pbleaves_pbadd_prop1 : forall a a1 l1, distinct_pbleaves (pbadd a1 (pbleaf a) l1).
proof: Proof. intros a a1 l1; generalize a a1; elim l1; simpl in |- *; auto; clear a a1 l1. intros a2; case a2; auto. Qed.
imports: Coq(List Compare_dec Sorting.Permutation) Huffman(AuxLib Code Build ISort UniqueKey)