proposition: Lemma In_KeyBasedPartition_fst : forall {TValue} k k' (m: t TValue), In k' (fst (partition (KeyBasedPartitioningFunction TValue k) m)) -> E.eq k k'.
proof: Proof. intros * in_singleton. apply In_MapsTo in in_singleton. destruct in_singleton as [ val (maps_to & _) ]. eapply MapsTo_KeyBasedPartition_fst; 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