proposition: Lemma StringMapsTo_fold_left A C : forall (f : A -> string) (f' : A -> C) l st idx, NoDup (map f l) -> In idx l -> StringMap.MapsTo (f idx) (f' idx) (fold_left (fun acc (el : A) => [f el |> f' el] :: acc ) l st).
proof: Proof. induction l; simpl; intros. - intuition. - intuition; subst. + rewrite fold_left_add2_Eq. apply StringMap.add_1; eauto. inversion H; subst. assert (~ StringMap.In (f idx) (StringMap.empty C)) by (rewrite empty_in_iff; tauto). remember (StringMap.empty C). generalize t H2 H0; clear; induction l; simpl; intros. * eauto. * intuition. eapply IHl; eauto. eapply StringMap_In_Permutation'. 2:eauto. intros. destruct H2. eapply add_mapsto_iff in H2; intuition. eexists; eauto. + inversion H; subst; eapply IHl; 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