proposition: Theorem frequency_list_restric_code_map : forall c, map (fst (B:=_)) (frequency_list A_eq_dec m) = map (fst (B:=_)) (restrict_code m c).
proof: Proof. intros c; unfold restrict_code in |- *; elim (frequency_list A_eq_dec m); simpl in |- *; auto. intros a0 l H; apply f_equal2 with (f := cons (A:=A)); auto. Qed.
imports: Coq(Sorting.Permutation)