proposition: Theorem in_frequency_map : forall l a, In a l -> In a (map fst (frequency_list l)).
proof: Proof. intros l; elim l; simpl in |- *; auto. intros a l0 H a0 [H0| H0]; auto. rewrite H0; elim (frequency_list l0); simpl in |- *; auto. intros (a1, l1) l2; simpl in |- *; auto. case (A_eq_dec a0 a1); simpl in |- *; auto. cut (In a0 (map (fst (A:=A) (B:=nat)) (frequency_list l0))); auto. elim (frequency_list l0); simpl in |- *; auto. intros (a1, l1) l2; simpl in |- *; auto. case (A_eq_dec a a1); simpl in |- *; auto. intros e H1 [H2| H2]; auto; left; rewrite <- H2; auto. intros e H1 [H2| H2]; auto. Qed.
imports: Coq(List Sorting.Permutation) Huffman(AuxLib UniqueKey)