proposition: Theorem NoDup_pbadd_prop2 : forall a1 l1 t, ~ inpb (pbleaf a1) t -> NoDup (all_pbleaves t) -> NoDup (all_pbleaves (pbadd a1 t l1)).
proof: Proof. intros a1 l1; elim l1; simpl in |- *; auto using NoDup_cons,NoDup_nil. intros b; case b; simpl in |- *; auto. intros l H t; case t; simpl in |- *; auto. intros a H0 H1; rewrite all_pbleaves_pbleaf; simpl in |- *; auto using NoDup_cons,NoDup_nil. rewrite all_pbleaves_pbleaf; intros p H0 H1. apply NoDup_app; simpl in |- *; auto using NoDup_cons,NoDup_nil. intros a H2 [H3| H3]; auto; (case H0; rewrite H3); auto. apply all_pbleaves_inpb; auto. intros p p0 H0 H1; apply NoDup_app; auto. apply NoDup_app_inv_l with (1 := H1); auto. apply H. contradict H0; auto. apply NoDup_app_inv_r with (1 := H1); auto. intros a H2 H3; case all_pbleaves_pbadd with (1 := H3). intros H4; contradict H0; rewrite <- H4; apply all_pbleaves_inpb; simpl in |- *; auto with datatypes. intros H4; apply NoDup_app_inv with (1 := H1) (a := a); auto. intros l H t; case t; simpl in |- *; auto. intros a H0 H1; rewrite all_pbleaves_pbleaf; simpl in |- *; auto using NoDup_cons,NoDup_nil. rewrite all_pbleaves_pbleaf; intros p H0 H1. apply NoDup_app; simpl in |- *; auto using NoDup_cons,NoDup_nil. intros a [H3| H3] H2; auto; (case H0; rewrite H3); auto. apply all_pbleaves_inpb; auto. intros p p0 H0 H1; apply NoDup_app; auto. apply H. contradict H0; auto. apply NoDup_app_inv_l with (1 := H1); auto. apply NoDup_app_inv_r with (1 := H1); auto. intros a H2 H3; case all_pbleaves_pbadd with (1 := H2). intros H4; contradict H0; rewrite <- H4; apply all_pbleaves_inpb; simpl in |- *; auto with datatypes. intros H4; apply NoDup_app_inv with (1 := H1) (a := a); auto. Qed.
imports: Coq(List Compare_dec Sorting.Permutation) Huffman(AuxLib Code Build ISort UniqueKey)