proposition: Lemma StringMap_In_Permutation {B C} : forall f f' l st st' k, let f' := (fun (acc : @StringMap.t C) (el : B) => StringMap.add (f el) (f' el) acc) in (forall k, StringMap.In k st -> StringMap.In k st') -> StringMap.In k (fold_left f' l st) -> StringMap.In k (fold_left f' l st').
proof: Proof. induction l; simpl; intros. - eauto. - eapply IHl. 2: apply H0. intros; destruct H1. apply add_mapsto_iff in H1; intuition; subst. eexists; apply StringMap.add_1; eauto. destruct (H k0). eexists; eauto. eexists x0. apply StringMap.add_2; 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