proposition: Lemma AbsR_add_EnsembleInsertRemove {A} : forall nr or kv, EnsembleFMapEquivalence (A := A) or nr -> EnsembleFMapEquivalence (EnsembleInsert kv (EnsembleRemoveKey (fst kv) or)) (StringIndexedMap.add (fst kv) (snd kv) nr).
proof: Proof. unfold SubEnsembleInsert, EnsembleRemoveKey, EnsembleInsert, EnsembleFMapEquivalence; intros; intuition. destruct (string_dec k a); subst; simpl in *. rewrite (StringIndexedMap.find_1 (StringIndexedMap.add_1 _ b (refl_equal a))) in H0; left; f_equal; congruence. right; intuition; apply StringIndexedMap.find_2 in H0; apply StringIndexedMap.add_3 in H0; eauto. eapply H; eauto using StringIndexedMap.find_1. unfold StringIndexedMap.In, StringIndexedMap.Raw.In0, StringIndexedMap.MapsTo in *; simpl in *; eauto. injections. eauto using StringIndexedMap.find_1, StringIndexedMap.add_1. apply H in H2; simpl in *. apply StringIndexedMap.find_1; apply StringIndexedMap.add_2; eauto. eauto using StringIndexedMap.find_1, StringIndexedMap.add_2, StringIndexedMap.remove_2, StringIndexedMap.find_2. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Strings.String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles Computation ADT ADTRefinement ADTNotation BuildADTRefinements KVEnsembles CacheSpec CacheRefinements String_as_OT FMapAVL