proposition: Theorem distinct_pbleaves_pbleaf : forall a : A, distinct_pbleaves (pbleaf a).
proof: Proof. intros a; red in |- *. intros a0 t1 t2 H; inversion H. Qed.
imports: Coq(List Compare_dec Sorting.Permutation) Huffman(AuxLib Code Build ISort UniqueKey)