proposition: Theorem inpbleaf_eq : forall a1 a2 a3 l, inpb (pbleaf a1) (pbadd a2 (pbleaf a3) l) -> a1 = a2.
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 H; inversion H; auto. intros a; case a. intros l H a1 a2 a3 H0; apply (H a1 a2 empty). inversion H0; auto. intros l H a1 a2 a3 H0; apply (H a1 a2 empty). inversion H0; auto. Qed.
imports: Coq(List Compare_dec Sorting.Permutation) Huffman(AuxLib Code Build ISort UniqueKey)