proposition: Lemma StringMapsTo_fold_left_ex A C : forall (f : A -> string) (f' : A -> C) l k v, ListFacts1.IsInjection f -> NoDup (map f l) -> StringMap.MapsTo k v (fold_left (fun acc (el : A) => [f el |> f' el] :: acc ) l (StringMap.empty _)) -> exists idx, k = f idx /\ v = f' idx.
proof: Proof. induction l; simpl; intros. - apply StringMap.empty_1 in H1; intuition. - inversion H0; subst. rewrite fold_left_add2_Eq in H1. rewrite add_mapsto_iff in H1; intuition. subst; eauto. eapply NIn_StringMap_fold_left; eauto. intro; apply H4; apply in_map_iff; eauto. rewrite empty_in_iff; tauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.ADT.Core Bedrock.Platform.Facade.DFModule Fiat.ADTNotation Bedrock.Platform.Facade.CompileUnit2 Fiat.Common.i3list Fiat.Common.ilist3 CertifiedExtraction.Core CertifiedExtraction.FacadeUtils CertifiedExtraction.StringMapUtils CertifiedExtraction.Extraction.Internal CertifiedExtraction.Extraction.Extraction