proposition: Lemma find_minimum_Key_In : forall indices kv, find_minimum_Key indices = Some kv -> StringIndexedMap.MapsTo (elt:=nat) (fst kv) (snd kv) indices.
proof: Proof. intros. unfold find_minimum_Key in H. rewrite StringIndexedMap.fold_1 in H. eapply StringIndexedMap.elements_2. destruct (@fold_left_In (StringIndexedMap.elements (elt:=nat) indices) kv None); intuition. unfold StringIndexedMap.key in *. rewrite <- H; f_equal. repeat (apply functional_extensionality; intros); f_equal; intuition. discriminate. destruct kv. unfold StringIndexedMap.eq_key_elt, StringIndexedMap.Raw.Proofs.PX.eqke; 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