proposition: Lemma AbsR_add_EnsembleUpdateKey' {A} : forall nr k f or, EnsembleFMapEquivalence or nr -> StringIndexedMap.find (elt:=A) k nr = None -> EnsembleFMapEquivalence (EnsembleUpdateKey k or f) nr.
proof: Proof. unfold EnsembleUpdateKey, EnsembleRemoveKey, EnsembleFMapEquivalence; intros; intuition. destruct (string_dec k0 k); subst. rewrite H0 in H1; discriminate. right; intuition; eapply H; eauto. subst; simpl in *. destruct_ex; intuition; eapply H in H3; subst. destruct_ex; rewrite H0 in *; discriminate. eapply H; eauto. 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