proposition: Lemma StringMap_fold_left_Eq {B C} : forall f f' l st st', let f' := (fun (acc : @StringMap.t C) (el : B) => StringMap.add (f el) (f' el) acc) in StringMap.Equal st st' -> StringMap.Equal (fold_left f' l st) (fold_left f' l st').
proof: Proof. induction l. - simpl; eauto. - simpl; intros. eapply IHl; rewrite H; reflexivity. 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