proposition: Theorem all_pbleaves_NoDup : forall t, distinct_pbleaves t -> NoDup (all_pbleaves t).
proof: Proof. intros t; elim t; simpl in |- *; auto using NoDup_cons,NoDup_nil. intros p H H0; apply H; apply distinct_pbleaves_pl; auto. intros p H H0; apply H; apply distinct_pbleaves_pr; auto. intros b H b0 H0 H1; apply NoDup_app; auto. apply H; apply distinct_pbleaves_l with (1 := H1). apply H0; apply distinct_pbleaves_r with (1 := H1). intros a H2 H3; case (H1 (pbleaf a) b b0); auto. apply all_pbleaves_inpb with (1 := H2). apply all_pbleaves_inpb with (1 := H3). Qed.
imports: Coq(List Compare_dec Sorting.Permutation) Huffman(AuxLib Code Build ISort UniqueKey)