proposition: Theorem distinct_pbleaves_pbadd_prop2 : forall a1 l1 l, ~ inpb (pbleaf a1) l -> distinct_pbleaves l -> distinct_pbleaves (pbadd a1 l l1).
proof: Proof. intros a1 l1 l H H0; apply all_pbleaves_unique. apply NoDup_pbadd_prop2; auto. apply all_pbleaves_NoDup; auto. Qed.
imports: Coq(List Compare_dec Sorting.Permutation) Huffman(AuxLib Code Build ISort UniqueKey)