proposition: Theorem inpb_pbadd : forall a1 l1 t1, inpb (pbleaf a1) (pbadd a1 t1 l1).
proof: Proof. intros a1 l1; elim l1; simpl in |- *; auto. intros b; case b; simpl in |- *; auto. intros l H t1; (case t1; simpl in |- *; auto). intros l H t1; (case t1; simpl in |- *; auto). Qed.
imports: Coq(List Compare_dec Sorting.Permutation) Huffman(AuxLib Code Build ISort UniqueKey)