proposition: Theorem pb_unique_prefix : forall t : pbtree, distinct_pbleaves t -> unique_prefix (compute_pbcode t).
proof: Proof. intros t H1; split; try exact (pb_unique_prefix1 t); apply pb_unique_key; auto. Qed.
imports: Coq(List Compare_dec Sorting.Permutation) Huffman(AuxLib Code Build ISort UniqueKey)