proposition: Lemma Permutation_map_Values {A B} : forall (f : A -> B) m, Permutation (List.map f (Values m)) (Values (map f m)).
proof: Proof. unfold Values; intros. rewrite map_snd. apply Permutation_InA_cons; eauto using elements_3w. - pose proof (elements_3w m) as NoDupM. induction NoDupM; simpl in *; simpl; constructor; eauto. unfold not; intros; apply H; clear NoDupM IHNoDupM H; induction l; simpl in *; inversion H0; subst; eauto. - split; intros. apply elements_1. rewrite InA_Map in H; destruct H as [[k' v'] [eq_k In_k]]; destruct eq_k; simpl in *; subst. rewrite H; eauto using elements_2, map_1, In_InA, equiv_eq_key_elt. rewrite InA_Map. apply elements_2 in H. apply map_mapsto_iff in H; destruct H as [a [a_eq MapsTo_k]]; subst. apply elements_1 in MapsTo_k. rewrite InA_alt in MapsTo_k. destruct MapsTo_k as [[k' a'] [eq_k In_k]]. eexists; split; eauto. destruct eq_k; simpl in *; subst; constructor; eauto. Qed.
imports: Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.Program.Program Coq.Structures.OrderedTypeEx Fiat.Common Fiat.Common.SetEq Fiat.Common.SetEqProperties Fiat.Common.List.ListFacts Fiat.Common.List.ListMorphisms Fiat.Common.LogicFacts Fiat.Common.SetoidClassInstances