diff --git a/theories/typing/interp.v b/theories/typing/interp.v
index 84539f0adc7e87a65990749ece2074f3afdffb3e..bcc74bd006e7f214c257627b226c1452f4be2ba0 100644
--- a/theories/typing/interp.v
+++ b/theories/typing/interp.v
@@ -1,6 +1,6 @@
 (* ReLoC -- Relational logic for fine-grained concurrency *)
 (** Interpretations for System F_mu_ref types *)
-From iris.algebra Require Import list.
+From iris.algebra Require Export list.
 From reloc.typing Require Export types.
 From reloc.logic Require Import model.
 From Autosubst Require Import Autosubst.
@@ -31,7 +31,7 @@ Section semtypes.
   Qed.
 
   Program Fixpoint interp (Ï„ : type) : listC lty2C -n> lty2C :=
-    match Ï„ as _ return _ with
+    match Ï„ as _ return listC lty2C -n> lty2C with
     | TUnit => λne _, lty2_unit
     | TNat => λne _, lty2_int
     | TBool => λne _, lty2_bool
@@ -51,52 +51,32 @@ Section semtypes.
     apply I. by f_equiv.
   Defined.
 
-  Definition bin_log_related_def (E : coPset)
+  Definition bin_log_related (E : coPset)
              (Δ : list lty2) (Γ : stringmap type)
              (e e' : expr) (τ : type) : iProp Σ :=
-    fmap (λ τ, interp τ Δ) Γ ⊨ e << e' : (interp τ Δ).
-
-  Definition bin_log_related_aux : seal bin_log_related_def. Proof. by eexists. Qed.
-  Definition bin_log_related := unseal bin_log_related_aux.
-  Definition bin_log_related_eq : bin_log_related = bin_log_related_def :=
-    seal_eq bin_log_related_aux.
+    {E;fmap (λ τ, interp τ Δ) Γ} ⊨ e << e' : (interp τ Δ).
 
 End semtypes.
 
 Notation "'{' E ';' Δ ';' Γ '}' ⊨ e '≤log≤' e' : τ" :=
   (bin_log_related E Δ Γ e%E e'%E (τ)%F)
-  (at level 74, E at level 50, Δ at next level, Γ at next level, e, e' at next level,
-   Ï„ at level 98,
+  (at level 100, E at next level, Δ at next level, Γ at next level, e, e' at next level,
+   Ï„ at level 200,
    format "'[hv' '{' E ';'  Δ ';'  Γ '}'  ⊨  '/  ' e  '/' '≤log≤'  '/  ' e'  :  τ ']'").
 Notation "'{' Δ ';' Γ '}' ⊨ e '≤log≤' e' : τ" :=
   (bin_log_related ⊤ Δ Γ e%E e'%E (τ)%F)
-  (at level 74, Δ at level 50, Γ at next level, e, e' at next level,
-   Ï„ at level 98,
+  (at level 100, Δ at next level, Γ at next level, e, e' at next level,
+   Ï„ at level 200,
    format "'[hv' '{' Δ ';'  Γ '}'  ⊨  '/  ' e  '/' '≤log≤'  '/  ' e'  :  τ ']'").
-Notation "Γ ⊨ e '≤log≤' e' : τ" :=
-  (∀ Δ, bin_log_related ⊤ Δ Γ e%E e'%E (τ)%F)%I
-  (at level 74, e, e' at next level,
-   Ï„ at level 98,
-   format "'[hv' Γ  ⊨  '/  ' e  '/' '≤log≤'  '/  ' e'  :  τ ']'").
-(* TODO: 
-If I set the level for Ï„ at 98 then the 
-following wouldn't pass:
-
-Lemma refinement1 `{logrelG Σ} Γ :
-    Γ ⊨ #() ≤log≤ #() : (Unit → Unit) → TNat.
-
-If the level is 99 then the following is not parsed.
-
-
-   Lemma refinement1 `{logrelG Σ} Γ :
-    Γ ⊨ #() ≤log≤ #() : (Unit → Unit) → TNat -∗ True.
-*)
 
 Section props.
   Context `{relocG Σ}.
 
-  (* Lemma fupd_logrel E1 E2 Δ Γ e e' τ : *)
-  (*   ((|={E1,E2}=> ({E2;Δ;Γ} ⊨ e ≤log≤ e' : τ)) *)
-  (*    -∗ {E1;Δ;Γ} ⊨ e ≤log≤ e' : τ)%I. *)
+  Lemma fupd_logrel E1 E2 Δ Γ e e' τ :
+    ((|={E1,E2}=> {E2;Δ;Γ} ⊨ e ≤log≤ e' : τ)
+     -∗ {E1;Δ;Γ} ⊨ e ≤log≤ e' : τ)%I.
+  Proof. apply fupd_logrel. Qed.
 
 End props.
+
+Notation "⤉ Γ" := (Autosubst_Classes.subst (ren (+1)%nat) <$> Γ) (at level 10, format "⤉ Γ").
diff --git a/theories/typing/types.v b/theories/typing/types.v
index e90783e282d3a525f22a5a10a47d779e1378855e..a7a08a7277fb9f0df206009e92d25ecc15446894 100644
--- a/theories/typing/types.v
+++ b/theories/typing/types.v
@@ -1,7 +1,7 @@
 (* ReLoC -- Relational logic for fine-grained concurrency *)
 (** Typing for System F_mu_ref with existential types and concurrency *)
 From stdpp Require Export stringmap.
-From iris.heap_lang Require Export lang notation.
+From iris.heap_lang Require Export lang notation metatheory.
 From Autosubst Require Import Autosubst.
 
 (** * Types *)
@@ -77,11 +77,7 @@ Definition unpack : val := λ: "x" "y", "y" "x".
 
 (** Operation lifts *)
 Instance insert_binder (A : Type): Insert binder A (stringmap A) :=
-  fun k τ Γ =>
-    match k with
-    | BAnon => Γ
-    | BNamed x => <[x:=τ]>Γ
-    end.
+  binder_insert.
 
 (** Typing itself *)
 Inductive typed (Γ : stringmap type) : expr → type → Prop :=