proposition: Lemma NIn_StringMap_fold_left A C : forall (f : A -> string) (f' : A -> C) l st idx, ~ In idx l -> ListFacts1.IsInjection f -> ~ StringMap.In (f idx) st -> ~ StringMap.In (f idx) (fold_left (fun acc (el : A) => [f el |> f' el] :: acc ) l st).
proof: Proof. induction l; simpl; intros. - intuition. - intuition; subst. apply IHl in H2; eauto. rewrite add_in_iff; intuition. apply H0 in H5; eauto. 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