proposition: Corollary StringMapsTo_fold_left' {n} C : forall (f : Fin.t n -> string) (f' : Fin.t n -> C) st idx, ListFacts1.IsInjection f -> StringMap.MapsTo (f idx) (f' idx) (fold_left (fun acc (el : Fin.t n) => [f el |> f' el] :: acc ) (BuildFinUpTo n) st).
proof: Proof. intros; eapply StringMapsTo_fold_left. - eapply ListFacts1.Injection_NoDup; eauto using NoDup_BuildFinUpTo. - eapply In_BuildFinUpTo. 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