proposition: Lemma FMap_fold_add_MapsTo_NIn {Value} : forall (f : Value -> Value) l k v bag', ~ InA (@eq_key _) (k,v) (List.map (fun kv => (fst kv, f (snd kv))) l) -> (MapsTo k v (fold_left (fun a p => add (fst p) (f (snd p)) a) l bag') <-> MapsTo k v bag').
proof: Proof. unfold eq_key; intros; revert k v bag' H. induction l; simpl; intros; split; eauto. intros; assert (MapsTo k v (add (fst a) (f (snd a)) bag')). apply IHl; [unfold not; intros; apply H; constructor 2; eauto | eauto]. apply add_mapsto_iff in H1; intuition; subst. intros; eapply IHl; eauto using add_2. 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