proposition: Theorem all_pbleaves_unique : forall t, NoDup (all_pbleaves t) -> distinct_pbleaves t.
proof: Proof. intros t; elim t; simpl in |- *; auto. intros b H b0 H0 H1; red in |- *. intros t0 t1 t2 H2; inversion H2. intros H4 H7; case (inpb_ex t0); intros a HH. apply NoDup_app_inv with (a := a) (1 := H1); auto; apply all_pbleaves_in; apply inpb_trans with (1 := HH); auto. apply H; auto; try apply NoDup_app_inv_l with (1 := H1). apply H0; auto; try apply NoDup_app_inv_r with (1 := H1). Qed.
imports: Coq(List Compare_dec Sorting.Permutation) Huffman(AuxLib Code Build ISort UniqueKey)