proposition: Lemma SameValues_remove2 av : forall k k' st', StringMap.Equal (StringMap.remove (elt:=Value av) k (StringMap.remove (elt:=Value av) k' st')) (StringMap.remove (elt:=Value av) k' (StringMap.remove (elt:=Value av) k st')).
proof: Proof. unfold StringMap.Equal. intros; repeat rewrite remove_o. repeat find_if_inside; 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