proposition: Lemma FMap_fold_add_MapsTo_In {Value} : forall (f : Value -> Value) (bag : t Value) bag' k v, InA (@eq_key_elt _) (k,v) (List.map (fun kv => (fst kv, f (snd kv))) (elements bag)) -> MapsTo k v (fold (fun k bag'' r' => add k (f bag'') r') bag bag').
proof: Proof. intros; rewrite fold_1 in *; revert k v bag' H; generalize (elements_3w bag); induction (elements bag); intros; inversion H0; inversion H; subst; simpl in *; eauto. destruct H2; simpl in *; subst; rewrite H1. apply FMap_fold_add_MapsTo_NIn; eauto. unfold not, eq_key in *; intros; apply H6; revert H2; clear; induction l; simpl in *; intros; inversion H2; subst; eauto. apply add_1; 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