proposition: Lemma AbsR_remove_EnsembleRemoveKey {A} : forall nr or k, EnsembleFMapEquivalence (A := A) or nr -> EnsembleFMapEquivalence (EnsembleRemoveKey k or) (StringIndexedMap.remove k nr).
proof: Proof. unfold EnsembleRemoveKey, EnsembleFMapEquivalence; intros; intuition; simpl in *; subst. eapply StringIndexedMap.remove_1; try reflexivity; unfold StringIndexedMap.In, StringIndexedMap.Raw.In0; simpl; apply StringIndexedMap.find_2 in H0; unfold StringIndexedMap.MapsTo, StringIndexedMap.remove in H0; simpl in H0; eauto. destruct (string_dec k0 k); subst; simpl in *. exfalso. eapply StringIndexedMap.remove_1; try reflexivity; unfold StringIndexedMap.In, StringIndexedMap.Raw.In0; simpl; apply StringIndexedMap.find_2 in H0; unfold StringIndexedMap.MapsTo, StringIndexedMap.remove in H0; simpl in H0; eauto. apply StringIndexedMap.find_2 in H0. apply StringIndexedMap.remove_3 in H0; eapply H; eauto using StringIndexedMap.find_1. apply StringIndexedMap.find_1. apply StringIndexedMap.remove_2; eauto. eapply H in H2. eauto using 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