proposition: Lemma MapsTo_partition_snd: forall TValue f k v (m: t TValue), Proper (E.eq ==> eq ==> eq) f -> MapsTo k v (snd (partition f m)) -> MapsTo k v m.
proof: Proof. intros * ? maps_to. rewrite partition_iff_2 with (f := f) (m := m) in maps_to; intuition. 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