proposition: Theorem inpb_pbadd_ex : forall a1 l1 t1 t, inpb t (pbadd a1 t1 l1) -> inpb (pbleaf a1) t \/ inpb t t1.
proof: Proof. intros a1 l1; elim l1; simpl in |- *; auto. intros t1 t H; inversion H; auto. intros a l H t1 t; case a; case t1; simpl in |- *; auto. intros a0 H0; inversion H0; auto. generalize H3 H; case l; simpl in |- *; auto. intros p H0; inversion H0; auto. left; generalize H3; elim l; simpl in |- *; auto. intros HH; inversion HH; auto. intros b; case b; simpl in |- *; auto. intros l0 H5 H6; inversion H6; auto. intros l0 H5 H6; inversion H6; auto. intros p H0; inversion H0; auto. case (H p t); auto. intros p p0 H0; inversion H0; auto. case (H p0 t); auto. intros a0 H0; inversion H0; auto. left; generalize H3; elim l; simpl in |- *; auto. intros HH; inversion HH; auto. intros b; case b; simpl in |- *; auto. intros l0 H5 H6; inversion H6; auto. intros l0 H5 H6; inversion H6; auto. intros p H0; inversion H0; auto. case (H p t); auto. intros p H0; inversion H0; auto. left; generalize H3; elim l; simpl in |- *; auto. intros HH; inversion HH; auto. intros b; case b; simpl in |- *; auto. intros l0 H5 H6; inversion H6; auto. intros l0 H5 H6; inversion H6; auto. intros p p0 H0; inversion H0; auto. case (H p t); auto. Qed.
imports: Coq(List Compare_dec Sorting.Permutation) Huffman(AuxLib Code Build ISort UniqueKey)