proposition: Theorem in_pbleaf_node : forall a1 a2 a3 a4 l, ~ inpb (pbnode a1 a2) (pbadd a3 (pbleaf a4) l).
proof: Proof. intros a1 a2 a3 a4 l; generalize a1 a2 a3 a4; elim l; simpl in |- *; auto; clear a1 a2 a3 a4 l. intros a1 a2 a3 a4; red in |- *; intros H; inversion H. intros a; case a. intros l H a1 a2 a3 a4; red in |- *; intros H0; case (H a1 a2 a3 empty). inversion H0; auto. intros l H a1 a2 a3 a4; red in |- *; intros H0; case (H a1 a2 a3 empty). inversion H0; auto. Qed.
imports: Coq(List Compare_dec Sorting.Permutation) Huffman(AuxLib Code Build ISort UniqueKey)