proposition: Theorem all_pbleaves_pbbuild : forall c, c <> [] -> unique_prefix c -> Permutation (map (fst (B:=_)) c) (all_pbleaves (pbbuild c)).
proof: Proof. intros c H H0; apply Permutation_trans with (map (fst (B:=_)) (compute_pbcode (pbbuild c))). apply Permutation_map. apply Permutation_sym; apply pbbuild_compute_perm; auto. apply all_pbleaves_compute_pb; auto. Qed.
imports: Coq(List Compare_dec Sorting.Permutation) Huffman(AuxLib Code Build ISort UniqueKey)