proposition: Theorem pbleaf_or_not : forall p, (exists a, p = pbleaf a) \/ (forall a : A, p <> pbleaf a).
proof: Proof. intros p; case p; simpl in |- *; try (intros; right; red in |- *; intros; discriminate). intros a; left; exists a; simpl in |- *; auto. Qed.
imports: Coq(List Compare_dec Sorting.Permutation) Huffman(AuxLib Code Build ISort UniqueKey)