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