proposition: Theorem restrict_not_null : forall c, m <> [] -> restrict_code m c <> [].
proof: Proof. case m; simpl in |- *; auto. unfold restrict_code in |- *. intros a0 l c H H1. absurd (In ((fun x : A * nat => (fst x, find_code A_eq_dec (fst x) c)) (a0, number_of_occurrences A_eq_dec a0 (a0 :: l))) []); auto with datatypes. rewrite <- H1. apply in_map with (f := fun x : A * nat => (fst x, find_code A_eq_dec (fst x) c)). apply frequency_number_of_occurrences; auto with datatypes. Qed.
imports: Coq(Sorting.Permutation)