proposition: Lemma SameValues_Pop_Both: forall `{FacadeWrapper (Value av) A} k ext tenv (st : State av) cmp (v: A), cmp ↝ v -> StringMap.remove k st ≲ tenv ∪ ext -> [k |> wrap v] :: st ≲ [[ `k ~~> cmp as _ ]] :: tenv ∪ ext.
proof: Proof. intros; simpl; repeat (StringMap_t || cleanup || eexists); eauto. Qed.
imports: CertifiedExtraction.HintDBs CertifiedExtraction.Core CertifiedExtraction.Utils CertifiedExtraction.StringMapUtils Coq.Setoids.Setoid