proposition: Lemma in_elements_after_add': forall {A: Type} _key (added elem: A) tree, (~ In _key tree) -> (elem = added \/ List.In elem (GetValues tree)) -> (List.In elem (GetValues (add _key added tree))).
proof: Proof. unfold GetValues; intros ? ? ? ? ? not_in is_in; rewrite <- MapsTo_snd; rewrite <- MapsTo_snd in is_in. setoid_rewrite add_mapsto_iff; destruct is_in as [eq | [_key' _key'_map]]; [ exists _key | exists _key'; right; split; [ intro Eeq; apply MapsTo_In in _key'_map; apply not_in; rewrite (In_iff _ Eeq) | ] ]; intuition. 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