proposition: Theorem inpb_pbbuild_inv : forall a c, c <> [] -> inpb (pbleaf a) (pbbuild c) -> exists l, In (a, l) c.
proof: Proof. intros a c; generalize a; elim c; simpl in |- *; auto. intros a0 H; elim H; auto. intros (a1, l1). intros l; case l. simpl in |- *; auto. unfold pbbuild in |- *; simpl in |- *; intros H a0 H0 H1; exists l1; left; apply f_equal2 with (f := pair (A:=A) (B:=list bool)); auto. apply sym_equal; apply inpbleaf_eq with (1 := H1). unfold pbbuild in |- *; simpl in |- *; intros p l0 H a0 H0 H1. case inpbleaf_pbadd_inv with (1 := H1); auto; intros H2. exists l1; left; apply f_equal2 with (f := pair (A:=A) (B:=list bool)); auto. case (H a0); auto. red in |- *; intros H3; discriminate. intros x H3; exists x; simpl in |- *; auto. Qed.
imports: Coq(List Compare_dec Sorting.Permutation) Huffman(AuxLib Code Build ISort UniqueKey)