proposition: Lemma StringMap_remove_add av: forall k v rest tenv ext, rest ≲ tenv ∪ ext -> k ∉ rest -> StringMap.remove (elt:=Value av) k ([k |> v ]:: rest) ≲ tenv ∪ ext.
proof: Proof. intros; eapply SameValues_Equal with (m1 := rest). unfold StringMap.Equal. intros; destruct (string_dec y k); subst. intros; symmetry; rewrite remove_eq_o; eauto. symmetry; rewrite <- not_find_in_iff; eauto. rewrite StringMapFacts.remove_neq_o; eauto. rewrite StringMapFacts.add_neq_o; eauto. 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