diff --git a/theories/examples/or.v b/theories/examples/or.v
index c7888b3758b2aa85779104150d044ebb43ff59da..62112cd78c008aa0fa4a23981483d4f3ff06e85f 100644
--- a/theories/examples/or.v
+++ b/theories/examples/or.v
@@ -2,7 +2,7 @@
 (** (In)equational theory of erratic choice operator (`or`). *)
 From iris.proofmode Require Import tactics.
 From iris.heap_lang.lib Require Export par.
-From reloc Require Export proofmode examples.Y (* for bot *).
+From reloc Require Export proofmode lib.Y (* for bot *).
 
 (** (Binary) non-determinism can be simluated with concurrency. In
 this file we derive the algebraic laws for parallel "or"/demonic
diff --git a/theories/logic/model.v b/theories/logic/model.v
index 08bad255b01119327ce24f6ca9aa9ea4fc9b0fde..0a5a020baf2d2af663677afb702d47686990a25d 100644
--- a/theories/logic/model.v
+++ b/theories/logic/model.v
@@ -114,16 +114,16 @@ Section semtypes.
     ∃ A, C A w1 w2)%I.
 
   (** The lty2 constructors are non-expansive *)
-  Instance lty2_prod_ne n : Proper (dist n ==> dist n ==> dist n) lty2_prod.
+  Global Instance lty2_prod_ne n : Proper (dist n ==> dist n ==> dist n) lty2_prod.
   Proof. solve_proper. Qed.
 
-  Instance lty2_sum_ne n : Proper (dist n ==> dist n ==> dist n) lty2_sum.
+  Global Instance lty2_sum_ne n : Proper (dist n ==> dist n ==> dist n) lty2_sum.
   Proof. solve_proper. Qed.
 
-  Instance lty2_arr_ne n : Proper (dist n ==> dist n ==> dist n) lty2_arr.
+  Global Instance lty2_arr_ne n : Proper (dist n ==> dist n ==> dist n) lty2_arr.
   Proof. solve_proper. Qed.
 
-  Instance lty2_rec_ne n : Proper (dist n ==> dist n)
+  Global Instance lty2_rec_ne n : Proper (dist n ==> dist n)
        (lty2_rec : (lty2C Σ -n> lty2C Σ) -> lty2C Σ).
   Proof.
     intros F F' HF.
diff --git a/theories/typing/interp.v b/theories/typing/interp.v
index ecce2767f4d1228f8e3ed67bd6e40a795a956c21..1ff154fcf3cab603555b3690c7c8fd432ce57a39 100644
--- a/theories/typing/interp.v
+++ b/theories/typing/interp.v
@@ -54,11 +54,6 @@ Section semtypes.
     apply lty2_rec_ne=> X /=.
     apply I. by f_equiv.
   Defined.
-  Next Obligation.
-    intros I τ τ' n Δ Δ' HΔ' ??.
-    rewrite /lty2_forall /lty2_car /=.
-    solve_proper.
-  Defined.
 
   Lemma unboxed_type_sound τ Δ v v' :
     UnboxedType τ →