proposition: Theorem distinct_pbleaves_pbright : forall t, distinct_pbleaves t -> distinct_pbleaves (pbright t).
proof: Proof. intros t H; red in |- *. intros a t1 t2 H0 H1 H2; apply (H a t1 t2); auto. inversion H0; auto. Qed.
imports: Coq(List Compare_dec Sorting.Permutation) Huffman(AuxLib Code Build ISort UniqueKey)