proposition: Lemma InA_mapsto_add' {Value} : forall bag' kv k' (v' : Value), (eq_key_elt kv (k', v') \/ (~ E.eq (fst kv) k' /\ InA (@eq_key_elt _) kv (elements bag'))) -> InA (@eq_key_elt _) kv (elements (add k' v' bag')).
proof: Proof. intros; destruct kv as [k v]; apply elements_1; apply add_mapsto_iff; intuition; [destruct H0; eauto | right; intuition; apply elements_2; 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