proposition: Lemma map_list_map_fmap: forall {A B: Type} m (proc: A -> B), SetEq (GetValues (map proc m)) (List.map proc (GetValues m)).
proof: Proof. unfold GetValues; split; intros. apply in_elements_after_map in H; destruct H as [k [predecessor (maps_to, is_predecessor)]]; rewrite in_map_iff; exists predecessor; subst; intuition; apply (InA_In_snd k), elements_1; trivial. rewrite in_map_iff in H; destruct H as [x0 (?, H)]; rewrite in_map_iff in H; destruct H as [x1 (is_pred, ?)]. apply (InA_In_snd (fst x1)); rewrite <- elements_mapsto_iff; apply map_mapsto_iff; exists x0; split; [ | apply in_elements_mapsto; rewrite <- is_pred, <- surjective_pairing ]; subst; congruence. 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