proposition: Theorem restrict_code_pbbuild : forall c : code A, not_null c -> unique_prefix c -> in_alphabet m c -> m <> [] -> Permutation (map fst (frequency_list A_eq_dec m)) (all_pbleaves (pbbuild empty (restrict_code m c))).
proof: Proof. intros c H H0 H1 H2. rewrite frequency_list_restric_code_map with (c := c). apply all_pbleaves_pbbuild; auto. apply restrict_not_null; auto. apply restrict_unique_prefix; auto. Qed.
imports: Coq(Sorting.Permutation)