proposition: Lemma map_modulo_equiv : forall {A B: Type} (db: t A) (seq: list A), SameElements seq db -> forall (proc: A -> B), SameElements (List.map proc seq) (map proc db).
proof: Proof. unfold SameElements; intros. rewrite (@map_modulo_SetEq _ _ _ (GetValues db)); trivial. clear H; clear seq. unfold SetEq. symmetry. apply map_list_map_fmap. 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