proposition: Lemma SameValues_PopExt': forall `{FacadeWrapper (Value av) A} (key : StringMap.key) (tail : Telescope av) (v0 : A) (ext initial_state : StringMap.t (Value av)), key ∉ ext -> initial_state ≲ tail ∪ [key |> wrap v0]::ext -> StringMap.remove key initial_state ≲ tail ∪ ext.
proof: Proof. intros. change tail with ((fun (_: A) => tail) v0). eauto using SameValues_PopExt. Qed.
imports: Coq.Classes.Morphisms CertifiedExtraction.CoreLemmas CertifiedExtraction.PropertiesOfTelescopes