proposition: Lemma SameValues_PushExt: forall `{FacadeWrapper (Value av) A} (key : StringMap.key) (tail : A -> Telescope av) (v0 : A) (ext initial_state : StringMap.t (Value av)), StringMap.MapsTo key (wrap v0) initial_state -> StringMap.remove key initial_state ≲ tail v0 ∪ ext -> initial_state ≲ tail v0 ∪ [key |> wrap v0]::ext.
proof: Proof. intros until v0. induction (tail v0) as [ | ? k ? ? IH ]; intros. - simpl in *; lazymatch goal with | [ H: StringMap.MapsTo _ _ _ |- _ ] => rewrite (MapsTo_add_remove H) end; eauto using WeakEq_add. - simpl in *. destruct k; push_pop IH. Qed.
imports: Coq.Classes.Morphisms CertifiedExtraction.CoreLemmas CertifiedExtraction.PropertiesOfTelescopes