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