proposition: Lemma SameValues_Mutation_helper: forall (av : Type) (vsrc vret : StringMap.key) (ext : StringMap.t (Value av)) (tenv : Telescope av) (initial_state : State av) (x : Value av), vret <> vsrc -> vret ∉ ext -> NotInTelescope vret tenv -> StringMap.MapsTo vsrc x initial_state -> initial_state ≲ tenv ∪ ext -> [vsrc |> x]::M.remove vret initial_state ≲ tenv ∪ ext.
proof: Proof. intros; rewrite <- remove_add_comm, <- add_redundant_cancel by congruence; facade_eauto. Qed.
imports: Coq.Lists.List CertifiedExtraction.Extraction.External.Core