proposition: Lemma StringIndexedMap_find_None_remove {V} : forall k k' m, StringIndexedMap.find (elt:=V) k m = None -> StringIndexedMap.find (elt:=V) k (StringIndexedMap.remove k' m) = None.
proof: Proof. intros. caseEq (StringIndexedMap.find (elt:=V) k (StringIndexedMap.remove (elt:=V) k' m)); eauto. apply StringIndexedMap.find_2 in H0. apply StringIndexedMap.remove_3 in H0; apply StringIndexedMap.find_1 in H0; congruence. 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