proposition: Theorem in_pbcompute_inpb : forall (t : pbtree) (a : A) (l : list bool), In (a, l) (compute_pbcode t) -> inpb (pbleaf a) t.
proof: Proof. intros t; elim t; simpl in |- *; auto. intros a a0 l [H1| H1]; try (case H1; fail). injection H1; intros H2 H3; rewrite H3; auto. intros p H a l H0; apply inpb_left; auto. case ((proj1 (in_map_iff _ _ _)) H0). intros (a1, l1) (Hl1, Ha1); apply (H a l1); auto. injection Hl1; intros HH1 HH2; rewrite <- HH2; auto. intros p H a l H0; apply inpb_right; auto. case ((proj1 (in_map_iff _ _ _)) H0). intros (a1, l1) (Hl1, Ha1); apply (H a l1); auto. injection Hl1; intros HH1 HH2; rewrite <- HH2; auto. intros h H h0 H0 a l H1. case in_app_or with (1 := H1); auto; intros H2. case ((proj1 (in_map_iff _ _ _)) H2). intros (a1, l1) (Hl1, Ha1); auto. apply inpb_node_l; apply (H a l1). injection Hl1; intros Hl2 Hl3; rewrite <- Hl3; auto. case ((proj1 (in_map_iff _ _ _)) H2). intros (a1, l1) (Hl1, Ha1); auto. apply inpb_node_r; apply (H0 a l1). injection Hl1; intros Hl2 Hl3; rewrite <- Hl3; auto. Qed.
imports: Coq(List Compare_dec Sorting.Permutation) Huffman(AuxLib Code Build ISort UniqueKey)