proposition: Theorem restrict_code_in : forall (m : list A) (a : A) (c : code A), In a m -> find_code A_eq_dec a c = find_code A_eq_dec a (restrict_code m c).
proof: Proof. intros m a c H. apply sym_equal; apply find_code_correct2; auto. apply restrict_code_unique_key. generalize (in_frequency_map _ A_eq_dec m a H). unfold restrict_code in |- *; elim (frequency_list A_eq_dec m); simpl in |- *; auto with datatypes. intros a0; case a0; simpl in |- *; auto with datatypes. intros a1 n l H0 [H1| H1]; try rewrite H1; auto. Qed.
imports: Coq(Sorting.Permutation)