proposition: Lemma in_elements_after_add: forall {A: Type} key (added elem: A) tree, (List.In elem (GetValues (add key added tree)) -> (elem = added \/ List.In elem (GetValues tree))).
proof: Proof. unfold GetValues; intros ? ? ? ? ? is_in; rewrite <- MapsTo_snd; rewrite <- MapsTo_snd in is_in. destruct is_in as [key' map_add]; rewrite add_mapsto_iff in map_add; destruct map_add; [ left | right ]; intuition; 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