proposition: Lemma indexBound_add_remove : forall indices k k' n, indexBound indices n -> indexBound (StringIndexedMap.add k n (StringIndexedMap.remove k' indices)) (S n).
proof: Proof. unfold indexBound; intros. destruct (string_dec k k0). rewrite (StringIndexedMap.find_1 (StringIndexedMap.add_1 _ _ e)) in H0. injections; omega. apply StringIndexedMap.find_2 in H0. eapply StringIndexedMap.add_3 in H0; eauto. destruct (string_dec k' k0). exfalso; eapply (StringIndexedMap.remove_1); eauto; unfold StringIndexedMap.In, StringIndexedMap.Raw.In0, StringIndexedMap.MapsTo in *; simpl in *; eauto. apply StringIndexedMap.remove_3 in H0; eauto. apply StringIndexedMap.find_1 in H0; 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