diff --git a/theories/logic/model.v b/theories/logic/model.v
index e10eacd968d5c3192527fbfe4360c90d2303b9a8..56c8e1cc3f03e03bbc5731c4ce7c1e483ebeb719 100644
--- a/theories/logic/model.v
+++ b/theories/logic/model.v
@@ -23,10 +23,10 @@ Existing Instance lty2_persistent.
 
 (* The COFE structure on semantic types *)
 Section lty2_ofe.
-  Context `{relocG Σ}.
+  Context `{invG Σ}.
 
-  Global Instance lty2_equiv : Equiv lty2 := λ A B, ∀ w1 w2, A w1 w2 ≡ B w1 w2.
-  Global Instance lty2_dist : Dist lty2 := λ n A B, ∀ w1 w2, A w1 w2 ≡{n}≡ B w1 w2.
+  Instance lty2_equiv : Equiv lty2 := λ A B, ∀ w1 w2, A w1 w2 ≡ B w1 w2.
+  Instance lty2_dist : Dist lty2 := λ n A B, ∀ w1 w2, A w1 w2 ≡{n}≡ B w1 w2.
   Lemma lty2_ofe_mixin : OfeMixin lty2.
   Proof. by apply (iso_ofe_mixin (lty2_car : lty2 → (val -c> val -c> iProp Σ))). Qed.
   Canonical Structure lty2C := OfeT lty2 lty2_ofe_mixin.
@@ -186,6 +186,17 @@ Section refinement.
     solve_proper.
   Qed.
 
+  (* TODO: this is a bit icky *)
+  Global Instance refines_proper E  :
+    Proper ((≡) ==> (=) ==> (=) ==> (≡) ==> (≡)) (refines E).
+  Proof.
+    intros Γ Γ' HΓ ? e -> ? e' -> A A' HA.
+    apply equiv_dist=>n.
+    setoid_rewrite equiv_dist in HA.
+    setoid_rewrite equiv_dist in HΓ.
+    by rewrite HA HΓ.
+  Defined.
+
 End refinement.
 
 Notation "⟦ A ⟧ₑ" := (λ e e', interp_expr ⊤ e e' A).