proposition: Theorem inpbleaf_pbadd_inv : forall a1 a2 a3 l, inpb (pbleaf a1) (pbadd a2 a3 l) -> a1 = a2 \/ inpb (pbleaf a1) a3.
proof: Proof. intros a1 a2 a3 l; generalize a1 a2 a3; elim l; simpl in |- *; auto; clear a1 a2 a3 l. intros a1 a2 a3 H0; inversion H0; auto. intros a; case a. intros l H a1 a2 a3; case a3; auto. intros a0 H0; left; apply (inpbleaf_eq a1 a2 empty l); auto. inversion H0; auto. intros p H1; inversion H1; auto. left; apply (inpbleaf_eq a1 a2 empty l); auto. intros p H0; case (H a1 a2 p); auto. inversion H0; auto. intros p p0 H1; inversion H1; auto. case (H a1 a2 p0); auto. intros l H a1 a2 a3; case a3; auto. intros a0 H1; left; apply (inpbleaf_eq a1 a2 empty l); auto. inversion H1; auto. intros p H1; case (H a1 a2 p); auto. inversion H1; auto. intros p H1; inversion H1. left; apply (inpbleaf_eq a1 a2 empty l); auto. case H0; auto. intros p p0 H1; inversion H1. case (H a1 a2 p); auto. case H0; auto. Qed.
imports: Coq(List Compare_dec Sorting.Permutation) Huffman(AuxLib Code Build ISort UniqueKey)