proposition: Lemma AbsR_add_EnsembleUpdateKey {A} : forall nr k f or v, EnsembleFMapEquivalence or nr -> StringIndexedMap.find (elt:=A) k nr = Some v -> EnsembleFMapEquivalence (EnsembleUpdateKey k or f) (StringIndexedMap.add k (f v) nr).
proof: Proof. unfold EnsembleUpdateKey, EnsembleRemoveKey, EnsembleFMapEquivalence; intros; intuition. destruct (string_dec k0 k); subst. left. rewrite (StringIndexedMap.find_1 (StringIndexedMap.add_1 nr (f v) (refl_equal k))) in *; simpl in *; f_equal; injections; intuition. eexists; split; eauto. eapply H; eauto. right; split; eauto. eapply H. eauto using StringIndexedMap.find_1, StringIndexedMap.add_3, StringIndexedMap.find_2. subst; simpl in *. destruct_ex; intuition; subst. apply H in H3; rewrite H0 in H3; injections. eauto using StringIndexedMap.find_1, StringIndexedMap.add_1. apply H in H3. eauto using StringIndexedMap.find_1, StringIndexedMap.add_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