proposition: Lemma KeyBasedPartition_fst_singleton : forall {TValue} k v (m: t TValue), MapsTo k v m -> Equal (fst (partition (KeyBasedPartitioningFunction TValue k) m)) (add k v (empty TValue)).
proof: Proof. intros. symmetry. unfold Equal; intro key. destruct (E.eq_dec key k) as [ eq_k_proj | neq_k_proj ]. rewrite eq_k_proj; rewrite add_eq_o by eauto; symmetry; rewrite <- find_mapsto_iff; rewrite partition_iff_1 with (f := KeyBasedPartitioningFunction TValue k) (m := m); intuition (try rewrite <- KeyBasedPartitioningFunction_eq_true; eauto using E.eq_refl, KeyBasedPartitioningFunction_Proper). rewrite add_neq_o by eauto. rewrite empty_o. destruct (find key _) eqn:eqfind'; [ exfalso | eauto ]. rewrite <- find_mapsto_iff in eqfind'. rewrite partition_iff_1 with (f := KeyBasedPartitioningFunction TValue k) (m := m) in eqfind'. destruct eqfind' as (maps_to & kvpf_true). apply neq_k_proj. erewrite KeyBasedPartitioningFunction_eq_true. rewrite KeyBasedPartitioningFunction_refl. eauto. eauto using KeyBasedPartitioningFunction_Proper. reflexivity. 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