proposition: Lemma MapsTo_KeyBasedPartition_fst : forall {TValue} k k' v (m: t TValue), MapsTo k' v (fst (partition (KeyBasedPartitioningFunction TValue k) m)) -> E.eq k k'.
proof: Proof. intros * maps_to. rewrite partition_iff_1 with (f := KeyBasedPartitioningFunction TValue k) (m := m) in maps_to; eauto using KeyBasedPartitioningFunction_Proper. destruct maps_to as (_ & kbpf_true). rewrite <- KeyBasedPartitioningFunction_eq_true in kbpf_true. trivial. 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