diff --git a/_CoqProject b/_CoqProject
index 717d5a672ab7b916c1bdad8b8127c2d0604eac95..bb31c07ca1de17c5678e0230cf6e0cc045220c7c 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -27,9 +27,11 @@ theories/proofmode.v
 theories/tests/tp_tests.v
 theories/tests/proofmode_tests.v
 
-theories/examples/lock.v
-theories/examples/counter.v
+theories/lib/lock.v
+theories/lib/counter.v
+theories/lib/Y.v
+
 theories/examples/bit.v
-theories/examples/Y.v
 theories/examples/or.v
 theories/examples/generative.v
+
diff --git a/theories/examples/generative.v b/theories/examples/generative.v
index 76573b33ecd8ec920e4dc1baef3a4433d40aafc4..d064b772ffa6f7816cfa07484ed77daef4de204f 100644
--- a/theories/examples/generative.v
+++ b/theories/examples/generative.v
@@ -6,7 +6,7 @@ Those are mostly "generative ADTs". *)
 From iris.proofmode Require Import tactics.
 From iris.heap_lang.lib Require Export par.
 From reloc Require Export proofmode prelude.bijections.
-From reloc.examples Require Export counter lock.
+From reloc.lib Require Export counter lock.
 From reloc.typing Require Export interp soundness.
 
 (** Using references for name generation *)
diff --git a/theories/examples/or.v b/theories/examples/or.v
index 4c3e4b1336740ccb118981716e31b4f62560eb9a..c7888b3758b2aa85779104150d044ebb43ff59da 100644
--- a/theories/examples/or.v
+++ b/theories/examples/or.v
@@ -79,6 +79,8 @@ Section rules.
       rel_load_r. repeat rel_pure_r. eauto with iFrame.
   Qed.
 
+  Opaque or.
+
   (** Compatibility rule *)
   Lemma or_compatible e1 e2 e1' e2' A :
     (REL e1 << e1' : () → A) -∗
@@ -89,7 +91,6 @@ Section rules.
     rel_bind_l e2. rel_bind_r e2'.
     iApply (refines_bind with "H2").
     iIntros (v2 v2') "#Hv2".
-    (* ^ TODO the arrow interpretation gets unfolded here *)
     rel_bind_l e1. rel_bind_r e1'.
     iApply (refines_bind with "H1").
     iIntros (v1 v1') "#Hv1". iSimpl.
diff --git a/theories/examples/Y.v b/theories/lib/Y.v
similarity index 100%
rename from theories/examples/Y.v
rename to theories/lib/Y.v
diff --git a/theories/examples/counter.v b/theories/lib/counter.v
similarity index 99%
rename from theories/examples/counter.v
rename to theories/lib/counter.v
index 1fa3816375bc3a8b40dde8dabcbaf572fc113974..7b7e23174736a18727b6a04392c2664db8a096fa 100644
--- a/theories/examples/counter.v
+++ b/theories/lib/counter.v
@@ -1,7 +1,7 @@
 From reloc Require Export proofmode.
 From reloc.typing Require Export types interp.
 From reloc.logic Require Import compatibility.
-From reloc.examples Require Import lock.
+From reloc.lib Require Import lock.
 From reloc.typing Require Import soundness.
 
 Definition CG_increment : val := λ: "x" "l",
diff --git a/theories/examples/lock.v b/theories/lib/lock.v
similarity index 100%
rename from theories/examples/lock.v
rename to theories/lib/lock.v
diff --git a/theories/logic/model.v b/theories/logic/model.v
index 843a06759a0c79921a24d3c177bad7dc54259271..08bad255b01119327ce24f6ca9aa9ea4fc9b0fde 100644
--- a/theories/logic/model.v
+++ b/theories/logic/model.v
@@ -139,7 +139,7 @@ Section semtypes.
 
 End semtypes.
 
-(* Nice notations *)
+(** Nice notations *)
 Notation "()" := lty2_unit : lty_scope.
 Infix "→" := lty2_arr : lty_scope.
 Infix "×" := lty2_prod (at level 80) : lty_scope.
@@ -242,13 +242,6 @@ End related_facts.
 Section monadic.
   Context `{relocG Σ}.
 
-  (* Lemma refines_ret_expr E e1 e2 A : *)
-  (*   interp_expr E e1 e2 A -∗ REL e1 << e2 @ E : A. *)
-  (* Proof. *)
-  (*   iIntros "HA". rewrite refines_eq /refines_def. *)
-  (*   eauto with iFrame. *)
-  (* Qed. *)
-
   Lemma refines_bind K K' E A A' e e' :
     (REL e << e' @ E : A) -∗
     (∀ v v', A v v' -∗
diff --git a/theories/typing/types.v b/theories/typing/types.v
index 8118cce7ecbd2940c79b1170adb43fb2c6832498..a4b524cd74cf5935e637027fce70a6ce43039ace 100644
--- a/theories/typing/types.v
+++ b/theories/typing/types.v
@@ -2,7 +2,7 @@
 (** (Syntactic) Typing for System F_mu_ref with existential types and concurrency *)
 From stdpp Require Export stringmap.
 From iris.heap_lang Require Export lang notation metatheory.
-From Autosubst Require Import Autosubst.
+From Autosubst Require Export Autosubst.
 
 (** * Types *)
 Inductive type :=