proposition: Theorem inpb_ex : forall t : pbtree, exists x, inpb (pbleaf x) t.
proof: Proof. intros t; elim t; simpl in |- *; auto. intros a; exists a; auto. intros b (a, H); exists a; auto. intros b (a, H); exists a; auto. intros b (a, H) b0 H0; exists a; auto. Qed.
imports: Coq(List Compare_dec Sorting.Permutation) Huffman(AuxLib Code Build ISort UniqueKey)