diff --git a/_CoqProject b/_CoqProject
index 6e4dad0219b4ba566db3c61600733707fe27c0b0..d7434e1c40c46908cc93c23d712e3e7dae5ed491 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -21,7 +21,7 @@ theories/typing/fundamental.v
 theories/typing/contextual_refinement.v
 theories/typing/soundness.v
 
-theories/proofmode.v
+theories/reloc.v
 
 theories/tests/tp_tests.v
 theories/tests/proofmode_tests.v
diff --git a/theories/examples/bit.v b/theories/examples/bit.v
index e24b31b6dd7e8aef814dd95bdbc6187dda46ffa7..a9c365781a25bf34e835424d777089231881f8e4 100644
--- a/theories/examples/bit.v
+++ b/theories/examples/bit.v
@@ -1,5 +1,5 @@
 From iris.proofmode Require Import tactics.
-From reloc Require Import proofmode.
+From reloc Require Import reloc.
 From reloc.typing Require Import types interp fundamental.
 From reloc.typing Require Import soundness.
 
@@ -30,7 +30,7 @@ Section bit_refinement.
     end.
 
   (* This is the graph of the `bitf` function *)
-  Definition bitτi : lty2 Σ := Lty2 (λ v1 v2,
+  Definition bitτi : lrel Σ := LRel (λ v1 v2,
     (∃ b : bool, ⌜v1 = #b⌝ ∗ ⌜v2 = #(bitf b)⌝))%I.
 
   Lemma bit_refinement Δ :
diff --git a/theories/examples/generative.v b/theories/examples/generative.v
index 8a1183b49fc3fc78e972427b99f694dbd3c37097..0befa62fb913c7a1b3293a608c749b8ba7679e6a 100644
--- a/theories/examples/generative.v
+++ b/theories/examples/generative.v
@@ -5,7 +5,7 @@ Ahmed, D. Dreyer, A. Rossberg.
 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 Require Export reloc prelude.bijections.
 From reloc.lib Require Export counter lock.
 From reloc.typing Require Export interp soundness.
 
@@ -29,7 +29,7 @@ Definition nameGen2 : expr :=
 Section namegen_refinement.
   Context `{relocG Σ, PrePBijG loc nat Σ}.
 
-  Program Definition ngR (γ : gname) : lty2 Σ := Lty2 (λ v1 v2,
+  Program Definition ngR (γ : gname) : lrel Σ := LRel (λ v1 v2,
    ∃ (l : loc) (n : nat), ⌜v1 = #l%V⌝ ∗ ⌜v2 = #n⌝
                          ∗ inBij γ l n)%I.
 
@@ -41,7 +41,7 @@ Section namegen_refinement.
                         end)%I.
 
   Lemma nameGen_ref1 :
-    REL nameGen1 << nameGen2 : ∃ α, (() → α) * (α → α → lty2_bool).
+    REL nameGen1 << nameGen2 : ∃ α, (() → α) * (α → α → lrel_bool).
   Proof.
     unlock nameGen1 nameGen2.
     rel_alloc_r c as "Hc".
@@ -151,15 +151,15 @@ Definition cell2 : expr :=
 Section cell_refinement.
   Context `{relocG Σ, lockG Σ}.
 
-  Definition lockR (R : lty2 Σ) (r1 r2 r3 r : loc) : iProp Σ :=
+  Definition lockR (R : lrel Σ) (r1 r2 r3 r : loc) : iProp Σ :=
     (∃ (a b c : val), r ↦ₛ a ∗ r2 ↦ b ∗ r3 ↦ c ∗
      ( (r1 ↦ #true ∗ R c a)
      ∨ (r1 ↦ #false ∗ R b a)))%I.
 
-  Definition cellInt (R : lty2 Σ) (r1 r2 r3 l r : loc) : iProp Σ :=
+  Definition cellInt (R : lrel Σ) (r1 r2 r3 l r : loc) : iProp Σ :=
     (∃ γ N, is_lock N γ #l (lockR R r1 r2 r3 r))%I.
 
-  Program Definition cellR (R : lty2 Σ) : lty2 Σ := Lty2 (λ v1 v2,
+  Program Definition cellR (R : lrel Σ) : lrel Σ := LRel (λ v1 v2,
     ∃ r1 r2 r3 l r : loc, ⌜v1 = (#r1, #r2, #r3, #l)%V⌝ ∗ ⌜v2 = #r⌝
      ∗ cellInt R r1 r2 r3 l r)%I.
 
diff --git a/theories/examples/or.v b/theories/examples/or.v
index 62112cd78c008aa0fa4a23981483d4f3ff06e85f..ff88965897d5c788656d1f74ada50e79659b2c1f 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 lib.Y (* for bot *).
+From reloc Require Export reloc 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/examples/symbol.v b/theories/examples/symbol.v
index 802e198ec72a195f819da02ac4c056b797c5097d..685b1f055730dbcde9a3c6cfd152be558b39053b 100644
--- a/theories/examples/symbol.v
+++ b/theories/examples/symbol.v
@@ -8,15 +8,14 @@ insert something into the table, we can show that the dynamic check in
 the lookup function in `symbol2` is redundant. *)
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth.
-From reloc Require Import proofmode.
+From reloc Require Import reloc.
 From reloc.lib Require Import lock list.
-From reloc.typing Require Import interp soundness.
 
 (** * Symbol table *)
-Definition lty_symbol `{relocG Σ} : lty2 Σ :=
-  ∃ α, (α → α → lty2_bool)    (* equality check *)
-     * (lty2_int → α)          (* insert *)
-     * (α → lty2_int).         (* lookup *)
+Definition lty_symbol `{relocG Σ} : lrel Σ :=
+  ∃ α, (α → α → lrel_bool)    (* equality check *)
+     * (lrel_int → α)          (* insert *)
+     * (α → lrel_int).         (* lookup *)
 
 Definition eqKey : val := λ: "n" "m", "n" = "m".
 Definition symbol1 : val := λ: <>,
@@ -100,14 +99,14 @@ Section rules.
     iApply inc_size'; by iFrame.
   Qed.
 
-  Definition tableR : lty2 Σ := Lty2 (λ v1 v2,
+  Definition tableR : lrel Σ := LRel (λ v1 v2,
     (∃ n : nat, ⌜v1 = #n⌝ ∗ ⌜v2 = #n⌝ ∗ own γ (◯ (n : mnat))))%I.
 
   Definition table_inv (size1 size2 tbl1 tbl2 : loc) : iProp Σ :=
     (∃ (n : nat) (ls : val), own γ (● (n : mnat))
                            ∗ size1 ↦{1/2} #n ∗ size2 ↦ₛ{1/2} #n
                            ∗ tbl1 ↦{1/2} ls ∗ tbl2 ↦ₛ{1/2} ls
-                           ∗ lty_list lty2_int ls ls)%I.
+                           ∗ lty_list lrel_int ls ls)%I.
 
   Definition lok_inv (size1 size2 tbl1 tbl2 l : loc) : iProp Σ :=
     (∃ (n : nat) (ls : val), size1 ↦{1/2} #n ∗ size2 ↦ₛ{1/2} #n
@@ -119,7 +118,7 @@ Section proof.
   Context `{!relocG Σ, !msizeG Σ, !lockG Σ}.
 
   Lemma eqKey_refinement γ :
-    REL eqKey << eqKey : tableR γ → tableR γ → lty2_bool.
+    REL eqKey << eqKey : tableR γ → tableR γ → lrel_bool.
   Proof.
     unlock eqKey.
     iApply refines_arrow_val.
@@ -141,7 +140,7 @@ Section proof.
       (λ: "n",
         let: "m" := ! #size2 in
          if: "n" ≤ "m" then (nth ! #tbl2) (! #size2 - "n") else #0)%V :
-      (tableR γ → lty2_int).
+      (tableR γ → lrel_int).
   Proof.
     iIntros "#Hinv".
     unlock. iApply refines_arrow_val.
@@ -180,7 +179,7 @@ Section proof.
         let: "m" := ! #size1 in
          if: "n" ≤ "m" then (nth ! #tbl1) (! #size1 - "n") else #0)%V
     <<
-      (λ: "n", (nth ! #tbl2) (! #size2 - "n"))%V : (tableR γ → lty2_int).
+      (λ: "n", (nth ! #tbl2) (! #size2 - "n"))%V : (tableR γ → lrel_int).
   Proof.
     iIntros "#Hinv".
     unlock.
diff --git a/theories/examples/ticket_lock.v b/theories/examples/ticket_lock.v
index c82ecac720898da988d1a9742886cc3593f6b95e..129a021e62e0fa17782c7d90d1515f4d5341a879 100644
--- a/theories/examples/ticket_lock.v
+++ b/theories/examples/ticket_lock.v
@@ -3,7 +3,7 @@
 From stdpp Require Import sets.
 From iris.algebra Require Export auth gset excl.
 From iris.base_logic Require Import auth.
-From reloc Require Import proofmode lib.lock lib.counter.
+From reloc Require Import reloc lib.lock lib.counter.
 From iris.heap_lang.lib Require Import ticket_lock.
 
 (* A different `acquire` funciton to showcase the atomic rule for FG_increment *)
@@ -13,8 +13,8 @@ Definition acquire : val := λ: "lk",
 (* A different `release` function to showcase the rule for wkincr *)
 Definition release : val := λ: "lk", wkincr (Fst "lk").
 
-Definition lty2_lock `{relocG Σ} : lty2 Σ :=
-  lty2_exists (λ A, (() → A) * (A → ()) * (A → ()))%lty2.
+Definition lrel_lock `{relocG Σ} : lrel Σ :=
+  lrel_exists (λ A, (() → A) * (A → ()) * (A → ()))%lrel.
 Definition lockT : type :=
   TExists (TProd (TProd (TUnit → TVar 0)
                         (TVar 0 → TUnit))
@@ -83,7 +83,7 @@ Section refinement.
 
   Definition N := relocN.@"locked".
 
-  Definition lockInt : lty2 Σ := Lty2 (λ v1 v2,
+  Definition lockInt : lrel Σ := LRel (λ v1 v2,
     ∃ (lo ln : loc) (γ : gname) (l' : loc),
         ⌜v1 = (#lo, #ln)%V⌝ ∗ ⌜v2 = #l'⌝
       ∗ inv N (lockInv lo ln γ l'))%I.
diff --git a/theories/lib/Y.v b/theories/lib/Y.v
index c7b4f8b88fb061186e60c77dd28526c447b8dd62..be43aaa921a3c527cc3ddf06bd84243640dd93b6 100644
--- a/theories/lib/Y.v
+++ b/theories/lib/Y.v
@@ -1,7 +1,7 @@
 (* ReLoC -- Relational logic for fine-grained concurrency *)
 (** Semantic typeability and equivalences for fixed point combinators. *)
 From iris.proofmode Require Import tactics.
-From reloc Require Export proofmode.
+From reloc Require Export reloc.
 
 Definition bot : val := rec: "bot" <> := "bot" #().
 
diff --git a/theories/lib/assert.v b/theories/lib/assert.v
index a6cc2c3d2848c7d9171116a1c99ee46f54508d3a..930db3385ec0ebdc66eb76c6ccc22c2697822f8a 100644
--- a/theories/lib/assert.v
+++ b/theories/lib/assert.v
@@ -1,7 +1,7 @@
 From iris.heap_lang Require Export lang.
 From iris.proofmode Require Import tactics.
 From iris.heap_lang.lib Require Export assert.
-From reloc Require Import proofmode.
+From reloc Require Import reloc.
 Set Default Proof Using "Type".
 
 Definition assert : val :=
diff --git a/theories/lib/counter.v b/theories/lib/counter.v
index e02c6500732823155beadd9b9ff914ca553a1fce..ad9536a26a5dcc31eb8d8abc84c6aaf2fb371ee7 100644
--- a/theories/lib/counter.v
+++ b/theories/lib/counter.v
@@ -1,4 +1,4 @@
-From reloc Require Export proofmode.
+From reloc Require Export reloc.
 From reloc.typing Require Export types interp.
 From reloc.logic Require Import compatibility.
 From reloc.lib Require Import lock.
@@ -147,7 +147,7 @@ Section CG_Counter.
 
   Lemma FG_CG_increment_refinement l cnt cnt' :
     inv counterN (counter_inv l cnt cnt') -∗
-    REL FG_increment #cnt << CG_increment #cnt' #l : lty2_int.
+    REL FG_increment #cnt << CG_increment #cnt' #l : lrel_int.
   Proof.
     iIntros "#Hinv".
     rel_apply_l
@@ -172,7 +172,7 @@ Section CG_Counter.
 
   Lemma counter_read_refinement l cnt cnt' :
     inv counterN (counter_inv l cnt cnt') -∗
-    REL counter_read #cnt << counter_read #cnt' : lty2_int.
+    REL counter_read #cnt << counter_read #cnt' : lrel_int.
   Proof.
     iIntros "#Hinv".
     rel_apply_l
@@ -194,7 +194,7 @@ Section CG_Counter.
   Qed.
 
   Lemma FG_CG_counter_refinement :
-    REL FG_counter << CG_counter : () → (() → lty2_int) * (() → lty2_int).
+    REL FG_counter << CG_counter : () → (() → lrel_int) * (() → lrel_int).
   Proof.
     unfold FG_counter, CG_counter. unlock.
     iApply refines_arrow_val.
diff --git a/theories/lib/list.v b/theories/lib/list.v
index a6a7b475306032c15bd79ca23c6ef74208948ce7..77c8e5585d05d2ff0119a21444b889682b4006b4 100644
--- a/theories/lib/list.v
+++ b/theories/lib/list.v
@@ -1,6 +1,6 @@
 (* ReLoC -- Relational logic for fine-grained concurrency *)
 (** Lists, their semantics types, and operations on them *)
-From reloc Require Import proofmode.
+From reloc Require Import reloc.
 From reloc.typing Require Import types interp.
 
 Notation CONS h t := (SOME (Pair h t)).
@@ -14,8 +14,8 @@ Fixpoint is_list (hd : val) (xs : list val) : Prop :=
   | x :: xs => ∃ hd', hd = CONSV x hd' ∧ is_list hd' xs
   end.
 
-Program Definition lty_list `{relocG Σ} (A : lty2 Σ) : lty2 Σ :=
-  lty2_rec (λne B, () + (A * B))%lty2.
+Program Definition lty_list `{relocG Σ} (A : lrel Σ) : lrel Σ :=
+  lrel_rec (λne B, () + (A * B))%lrel.
 Next Obligation. solve_proper. Qed.
 
 Definition nth : val := rec: "nth" "l" "n" :=
@@ -31,26 +31,26 @@ Lemma lty_list_nil `{relocG Σ} A :
 Proof.
   unfold lty_list.
   rewrite lty_rec_unfold /=.
-  unfold lty2_rec1 , lty2_car. (* TODO so much unfolding *)
+  unfold lrel_rec1 , lrel_car. (* TODO so much unfolding *)
   simpl. iNext.
   iExists _,_. iLeft. repeat iSplit; eauto.
 Qed.
 
-Lemma lty_list_cons `{relocG Σ} (A : lty2 Σ) v1 v2 ls1 ls2 :
+Lemma lty_list_cons `{relocG Σ} (A : lrel Σ) v1 v2 ls1 ls2 :
   A v1 v2 -∗
   lty_list A ls1 ls2 -∗
   lty_list A (CONSV v1 ls1) (CONSV v2 ls2).
 Proof.
   iIntros "#HA #Hls".
   rewrite {2}/lty_list lty_rec_unfold /=.
-  rewrite /lty2_rec1 {3}/lty2_car.
+  rewrite /lrel_rec1 {3}/lrel_car.
   iNext. simpl. iExists _, _.
   iRight. repeat iSplit; eauto.
-  rewrite {1}/lty2_prod /lty2_car /=.
+  rewrite {1}/lrel_prod /lrel_car /=.
   iExists _,_,_,_. repeat iSplit; eauto.
 Qed.
 
-Lemma refines_nth_l `{relocG Σ} (A : lty2 Σ) K v w ls (n: nat) t :
+Lemma refines_nth_l `{relocG Σ} (A : lrel Σ) K v w ls (n: nat) t :
   is_list v ls →
   ls !! n = Some w →
   (REL fill K (of_val w) << t : A) -∗
@@ -72,7 +72,7 @@ Proof.
       iApply "IH"; eauto.
 Qed.
 
-Lemma refines_nth_r `{relocG Σ} (A : lty2 Σ) K v w ls (n: nat) e :
+Lemma refines_nth_r `{relocG Σ} (A : lrel Σ) K v w ls (n: nat) e :
   is_list v ls →
   ls !! n = Some w →
   (REL e << fill K (of_val w) : A) -∗
@@ -95,5 +95,5 @@ Proof.
 Qed.
 
 Lemma nth_int_typed `{relocG Σ} :
-  REL nth << nth : lty_list lty2_int → lty2_int → lty2_int.
+  REL nth << nth : lty_list lrel_int → lrel_int → lrel_int.
 Proof. admit. Admitted.
diff --git a/theories/lib/lock.v b/theories/lib/lock.v
index e7712dd19c7c8657aceb21706a2765cbc144bd44..8b5a31bd5886dbe692bdf050d4f34da14a548193 100644
--- a/theories/lib/lock.v
+++ b/theories/lib/lock.v
@@ -1,6 +1,6 @@
 From iris.algebra Require Import excl.
 From reloc.typing Require Import types interp fundamental.
-From reloc Require Export proofmode.
+From reloc Require Export reloc.
 
 Definition newlock : val := λ: <>, ref #false.
 Definition acquire : val := rec: "acquire" "x" :=
diff --git a/theories/logic/adequacy.v b/theories/logic/adequacy.v
index 78803865628c93079fa432e2251db77b35e72932..865f180dfb62b3e140db2eaa8a491fb898f222c2 100644
--- a/theories/logic/adequacy.v
+++ b/theories/logic/adequacy.v
@@ -15,13 +15,13 @@ Definition relocΣ : gFunctors := #[heapΣ; authΣ cfgUR].
 Instance subG_relocPreG {Σ} : subG relocΣ Σ → relocPreG Σ.
 Proof. solve_inG. Qed.
 
-Definition pure_lty2 `{relocG Σ} (P : val → val → Prop) :=
-  @Lty2 Σ (λ v v', ⌜P v v'⌝)%I _.
+Definition pure_lrel `{relocG Σ} (P : val → val → Prop) :=
+  @LRel Σ (λ v v', ⌜P v v'⌝)%I _.
 
 Lemma refines_adequate Σ `{relocPreG Σ}
-  (A : ∀ `{relocG Σ}, lty2 Σ)
+  (A : ∀ `{relocG Σ}, lrel Σ)
   (P : val → val → Prop) e e' σ :
-  (∀ `{relocG Σ}, ∀ v v', A v v' -∗ pure_lty2 P v v') →
+  (∀ `{relocG Σ}, ∀ v v', A v v' -∗ pure_lrel P v v') →
   (∀ `{relocG Σ}, REL e << e' : A) →
   adequate NotStuck e σ
     (λ v _, ∃ thp' h v', rtc erased_step ([e'], σ) (of_val v' :: thp', h)
@@ -63,7 +63,7 @@ Proof.
 Qed.
 
 Theorem refines_typesafety Σ `{relocPreG Σ} e e' e1
-        (A : ∀ `{relocG Σ}, lty2 Σ) thp σ σ' :
+        (A : ∀ `{relocG Σ}, lrel Σ) thp σ σ' :
   (∀ `{relocG Σ}, REL e << e' : A) →
   rtc erased_step ([e], σ) (thp, σ') → e1 ∈ thp →
   is_Some (to_val e1) ∨ reducible e1 σ'.
diff --git a/theories/logic/compatibility.v b/theories/logic/compatibility.v
index b34bfb6e87195a4b62ac0f1d6720dc5ff5604e1b..3ed171b7252abd4cc47d3c64f080621a4cc2516e 100644
--- a/theories/logic/compatibility.v
+++ b/theories/logic/compatibility.v
@@ -58,7 +58,7 @@ Section compatibility.
     - iExists #(); eauto.
   Qed.
 
-  Lemma refines_exists (A : lty2 Σ) e e' (C : lty2 Σ → lty2 Σ) :
+  Lemma refines_exists (A : lrel Σ) e e' (C : lrel Σ → lrel Σ) :
     (REL e << e' : C A) -∗
     REL e << e' : ∃ A, C A.
   Proof.
diff --git a/theories/logic/derived.v b/theories/logic/derived.v
index f1266505a06ab3bd543e4e90f7c75ea239fe378d..90e668cbc27098ef2bab0f6c862e5763d74865e1 100644
--- a/theories/logic/derived.v
+++ b/theories/logic/derived.v
@@ -8,7 +8,7 @@ From reloc.logic Require Export model rules.
 
 Section rules.
   Context `{relocG Σ}.
-  Implicit Types A : lty2 Σ.
+  Implicit Types A : lrel Σ.
 
   Lemma refines_wand E e1 e2 A A' :
     (REL e1 << e2 @ E : A) -∗
@@ -26,7 +26,7 @@ Section rules.
     AsRecV v' f' x' eb' →
     □(∀ v1 v2 : val, □(REL of_val v1 << of_val v2 : A) -∗
       REL App v (of_val v1) << App v' (of_val v2) : A') -∗
-    REL v << v' : (A → A')%lty2.
+    REL v << v' : (A → A')%lrel.
   Proof.
     iIntros (??) "#H".
     iApply refines_arrow_val; eauto.
diff --git a/theories/logic/model.v b/theories/logic/model.v
index 53373432f6a71417f996580538cbf86e7245ec15..1be0b07cb524440fa2f71e5cc8103de5190168d8 100644
--- a/theories/logic/model.v
+++ b/theories/logic/model.v
@@ -12,29 +12,29 @@ From reloc Require Import prelude.properness logic.spec_rules prelude.ctx_subst.
 From reloc Require Export logic.spec_ra.
 
 (** Semantic intepretation of types *)
-Record lty2 Σ := Lty2 {
-  lty2_car :> val → val → iProp Σ;
-  lty2_persistent v1 v2 : Persistent (lty2_car v1 v2)
+Record lrel Σ := LRel {
+  lrel_car :> val → val → iProp Σ;
+  lrel_persistent v1 v2 : Persistent (lrel_car v1 v2)
 }.
-Arguments Lty2 {_} _%I {_}.
-Arguments lty2_car {_} _ _ _ : simpl never.
-Bind Scope lty_scope with lty2.
-Delimit Scope lty_scope with lty2.
-Existing Instance lty2_persistent.
+Arguments LRel {_} _%I {_}.
+Arguments lrel_car {_} _ _ _ : simpl never.
+Bind Scope lty_scope with lrel.
+Delimit Scope lty_scope with lrel.
+Existing Instance lrel_persistent.
 
 (* The COFE structure on semantic types *)
-Section lty2_ofe.
+Section lrel_ofe.
   Context `{Σ : gFunctors}.
 
-  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.
+  Instance lrel_equiv : Equiv (lrel Σ) := λ A B, ∀ w1 w2, A w1 w2 ≡ B w1 w2.
+  Instance lrel_dist : Dist (lrel Σ) := λ n A B, ∀ w1 w2, A w1 w2 ≡{n}≡ B w1 w2.
+  Lemma lrel_ofe_mixin : OfeMixin (lrel Σ).
+  Proof. by apply (iso_ofe_mixin (lrel_car : lrel Σ → (val -c> val -c> iProp Σ))). Qed.
+  Canonical Structure lrelC := OfeT (lrel Σ) lrel_ofe_mixin.
 
-  Global Instance lty2_cofe : Cofe lty2C.
+  Global Instance lrel_cofe : Cofe lrelC.
   Proof.
-    apply (iso_cofe_subtype' (λ A : val -c> val -c> iProp Σ, ∀ w1 w2, Persistent (A w1 w2)) (@Lty2 _) lty2_car)=>//.
+    apply (iso_cofe_subtype' (λ A : val -c> val -c> iProp Σ, ∀ w1 w2, Persistent (A w1 w2)) (@LRel _) lrel_car)=>//.
     - apply _.
     - apply limit_preserving_forall=> w1.
       apply limit_preserving_forall=> w2.
@@ -42,25 +42,25 @@ Section lty2_ofe.
       intros n P Q HPQ. apply (HPQ w1 w2).
   Qed.
 
-  Global Instance lty2_inhabited : Inhabited (lty2 Σ) := populate (Lty2 inhabitant).
+  Global Instance lrel_inhabited : Inhabited (lrel Σ) := populate (LRel inhabitant).
 
-  Global Instance lty2_car_ne n : Proper (dist n ==> (=) ==> (=) ==> dist n) lty2_car.
+  Global Instance lrel_car_ne n : Proper (dist n ==> (=) ==> (=) ==> dist n) lrel_car.
   Proof. by intros A A' ? w1 w2 <- ? ? <-. Qed.
-  Global Instance lty2_car_proper : Proper ((≡) ==> (=) ==> (=) ==> (≡)) lty2_car.
+  Global Instance lrel_car_proper : Proper ((≡) ==> (=) ==> (=) ==> (≡)) lrel_car.
   Proof. solve_proper_from_ne. Qed.
-End lty2_ofe.
+End lrel_ofe.
 
-Arguments lty2C : clear implicits.
+Arguments lrelC : clear implicits.
 
 Section semtypes.
   Context `{relocG Σ}.
 
   Implicit Types e : expr.
   Implicit Types E : coPset.
-  Implicit Types A B : lty2 Σ.
+  Implicit Types A B : lrel Σ.
 
   Definition refines_def (E : coPset)
-           (e e' : expr) (A : lty2 Σ) : iProp Σ :=
+           (e e' : expr) (A : lrel Σ) : iProp Σ :=
     (* TODO: refactor the quantifiers *)
     (∀ ρ, spec_ctx ρ -∗ (∀ j K, j ⤇ fill K e'
         ={E,⊤}=∗ WP e {{ v, ∃ v', j ⤇ fill K (of_val v') ∗ A v v' }}))%I.
@@ -78,91 +78,91 @@ Section semtypes.
     Proper ((=) ==> (=) ==> (≡) ==> (≡)) (refines E).
   Proof. solve_proper_from_ne. Qed.
 
-  Definition lty2_unit : lty2 Σ := Lty2 (λ w1 w2, ⌜ w1 = #() ∧ w2 = #() ⌝%I).
-  Definition lty2_bool : lty2 Σ := Lty2 (λ w1 w2, ∃ b : bool, ⌜ w1 = #b ∧ w2 = #b ⌝)%I.
-  Definition lty2_int : lty2 Σ := Lty2 (λ w1 w2, ∃ n : Z, ⌜ w1 = #n ∧ w2 = #n ⌝)%I.
+  Definition lrel_unit : lrel Σ := LRel (λ w1 w2, ⌜ w1 = #() ∧ w2 = #() ⌝%I).
+  Definition lrel_bool : lrel Σ := LRel (λ w1 w2, ∃ b : bool, ⌜ w1 = #b ∧ w2 = #b ⌝)%I.
+  Definition lrel_int : lrel Σ := LRel (λ w1 w2, ∃ n : Z, ⌜ w1 = #n ∧ w2 = #n ⌝)%I.
 
-  Definition lty2_arr (A1 A2 : lty2 Σ) : lty2 Σ := Lty2 (λ w1 w2,
+  Definition lrel_arr (A1 A2 : lrel Σ) : lrel Σ := LRel (λ w1 w2,
     □ ∀ v1 v2, A1 v1 v2 -∗ refines ⊤ (App w1 v1) (App w2 v2) A2)%I.
 
-  Definition lty2_ref (A : lty2 Σ) : lty2 Σ := Lty2 (λ w1 w2,
+  Definition lrel_ref (A : lrel Σ) : lrel Σ := LRel (λ w1 w2,
     ∃ l1 l2: loc, ⌜w1 = #l1⌝ ∧ ⌜w2 = #l2⌝ ∧
       inv (relocN .@ "ref" .@ (l1,l2)) (∃ v1 v2, l1 ↦ v1 ∗ l2 ↦ₛ v2 ∗ A v1 v2))%I.
 
-  Definition lty2_prod (A B : lty2 Σ) : lty2 Σ := Lty2 (λ w1 w2,
+  Definition lrel_prod (A B : lrel Σ) : lrel Σ := LRel (λ w1 w2,
     ∃ v1 v2 v1' v2', ⌜w1 = (v1,v1')%V⌝ ∧ ⌜w2 = (v2,v2')%V⌝ ∧
         A v1 v2 ∗ B v1' v2')%I.
 
-  Definition lty2_sum (A B : lty2 Σ) : lty2 Σ := Lty2 (λ w1 w2,
+  Definition lrel_sum (A B : lrel Σ) : lrel Σ := LRel (λ w1 w2,
     ∃ v1 v2, (⌜w1 = InjLV v1⌝ ∧ ⌜w2 = InjLV v2⌝ ∧ A v1 v2)
           ∨  (⌜w1 = InjRV v1⌝ ∧ ⌜w2 = InjRV v2⌝ ∧ B v1 v2))%I.
 
-  Definition lty2_rec1 (C : lty2C Σ -n> lty2C Σ) (rec : lty2 Σ) : lty2 Σ :=
-    Lty2 (λ w1 w2, ▷ C rec w1 w2)%I.
-  Instance lty2_rec1_contractive C : Contractive (lty2_rec1 C).
+  Definition lrel_rec1 (C : lrelC Σ -n> lrelC Σ) (rec : lrel Σ) : lrel Σ :=
+    LRel (λ w1 w2, ▷ C rec w1 w2)%I.
+  Instance lrel_rec1_contractive C : Contractive (lrel_rec1 C).
   Proof.
     intros n. intros P Q HPQ.
-    unfold lty2_rec1. intros w1 w2.
+    unfold lrel_rec1. intros w1 w2.
     apply bi.later_contractive.
     destruct n; try done.
     simpl in HPQ; simpl. f_equiv. by apply C.
   Qed.
 
-  Definition lty2_rec (C : lty2C Σ -n> lty2C Σ) : lty2 Σ := fixpoint (lty2_rec1 C).
+  Definition lrel_rec (C : lrelC Σ -n> lrelC Σ) : lrel Σ := fixpoint (lrel_rec1 C).
 
-  Definition lty2_exists (C : lty2 Σ → lty2 Σ) : lty2 Σ := Lty2 (λ w1 w2,
+  Definition lrel_exists (C : lrel Σ → lrel Σ) : lrel Σ := LRel (λ w1 w2,
     ∃ A, C A w1 w2)%I.
 
-  Definition lty2_forall (C : lty2 Σ → lty2 Σ) : lty2 Σ := Lty2 (λ w1 w2,
-    □ ∀ A : lty2 Σ, (lty2_arr lty2_unit (C A))%lty2 w1 w2)%I.
+  Definition lrel_forall (C : lrel Σ → lrel Σ) : lrel Σ := LRel (λ w1 w2,
+    □ ∀ A : lrel Σ, (lrel_arr lrel_unit (C A))%lrel w1 w2)%I.
 
-  Definition lty2_true : lty2 Σ := Lty2 (λ w1 w2, True)%I.
+  Definition lrel_true : lrel Σ := LRel (λ w1 w2, True)%I.
 
-  (** The lty2 constructors are non-expansive *)
-  Global Instance lty2_prod_ne n : Proper (dist n ==> dist n ==> dist n) lty2_prod.
+  (** The lrel constructors are non-expansive *)
+  Global Instance lrel_prod_ne n : Proper (dist n ==> dist n ==> dist n) lrel_prod.
   Proof. solve_proper. Qed.
 
-  Global Instance lty2_sum_ne n : Proper (dist n ==> dist n ==> dist n) lty2_sum.
+  Global Instance lrel_sum_ne n : Proper (dist n ==> dist n ==> dist n) lrel_sum.
   Proof. solve_proper. Qed.
 
-  Global Instance lty2_arr_ne n : Proper (dist n ==> dist n ==> dist n) lty2_arr.
+  Global Instance lrel_arr_ne n : Proper (dist n ==> dist n ==> dist n) lrel_arr.
   Proof. solve_proper. Qed.
 
-  Global Instance lty2_rec_ne n : Proper (dist n ==> dist n)
-       (lty2_rec : (lty2C Σ -n> lty2C Σ) -> lty2C Σ).
+  Global Instance lrel_rec_ne n : Proper (dist n ==> dist n)
+       (lrel_rec : (lrelC Σ -n> lrelC Σ) -> lrelC Σ).
   Proof.
     intros F F' HF.
-    unfold lty2_rec, lty2_car.
+    unfold lrel_rec, lrel_car.
     apply fixpoint_ne=> X w1 w2.
-    unfold lty2_rec1, lty2_car. cbn.
+    unfold lrel_rec1, lrel_car. cbn.
     f_equiv.
-    apply lty2_car_ne; eauto.
+    apply lrel_car_ne; eauto.
   Qed.
 
-  Lemma lty_rec_unfold (C : lty2C Σ -n> lty2C Σ) : lty2_rec C ≡ lty2_rec1 C (lty2_rec C).
+  Lemma lty_rec_unfold (C : lrelC Σ -n> lrelC Σ) : lrel_rec C ≡ lrel_rec1 C (lrel_rec C).
   Proof. apply fixpoint_unfold. Qed.
 
 End semtypes.
 
 (** Nice notations *)
-Notation "()" := lty2_unit : lty_scope.
-Infix "→" := lty2_arr : lty_scope.
-Infix "*" := lty2_prod : lty_scope.
-Infix "+" := lty2_sum : lty_scope.
-Notation "'ref' A" := (lty2_ref A) : lty_scope.
+Notation "()" := lrel_unit : lty_scope.
+Infix "→" := lrel_arr : lty_scope.
+Infix "*" := lrel_prod : lty_scope.
+Infix "+" := lrel_sum : lty_scope.
+Notation "'ref' A" := (lrel_ref A) : lty_scope.
 Notation "∃ A1 .. An , C" :=
-  (lty2_exists (λ A1, .. (lty2_exists (λ An, C%lty2)) ..)) : lty_scope.
+  (lrel_exists (λ A1, .. (lrel_exists (λ An, C%lrel)) ..)) : lty_scope.
 Notation "∀ A1 .. An , C" :=
-  (lty2_forall (λ A1, .. (lty2_forall (λ An, C%lty2)) ..)) : lty_scope.
+  (lrel_forall (λ A1, .. (lrel_forall (λ An, C%lrel)) ..)) : lty_scope.
 
 Section semtypes_properties.
   Context `{relocG Σ}.
 
   (* The reference type relation is functional and injective.
      Thanks to Amin. *)
-  Lemma interp_ref_funct E (A : lty2 Σ) (l l1 l2 : loc) :
+  Lemma interp_ref_funct E (A : lrel Σ) (l l1 l2 : loc) :
     ↑relocN ⊆ E →
-    (ref A)%lty2 #l #l1 ∗ (ref A)%lty2 #l #l2
+    (ref A)%lrel #l #l1 ∗ (ref A)%lrel #l #l2
     ={E}=∗ ⌜l1 = l2⌝.
   Proof.
     iIntros (?) "[Hl1 Hl2] /=".
@@ -176,9 +176,9 @@ Section semtypes_properties.
     compute in Hfoo. eauto.
   Qed.
 
-  Lemma interp_ref_inj E (A : lty2 Σ) (l l1 l2 : loc) :
+  Lemma interp_ref_inj E (A : lrel Σ) (l l1 l2 : loc) :
     ↑relocN ⊆ E →
-    (ref A)%lty2 #l1 #l ∗ (ref A)%lty2 #l2 #l
+    (ref A)%lrel #l1 #l ∗ (ref A)%lrel #l2 #l
     ={E}=∗ ⌜l1 = l2⌝.
   Proof.
     iIntros (?) "[Hl1 Hl2] /=".
@@ -195,12 +195,12 @@ Section semtypes_properties.
 End semtypes_properties.
 
 Notation "'REL' e1 '<<' e2 '@' E ':' A" :=
-  (refines E e1%E e2%E (A)%lty2)
+  (refines E e1%E e2%E (A)%lrel)
   (at level 100, E at next level, e1, e2 at next level,
    A at level 200,
    format "'[hv' 'REL'  e1  '/' '<<'  '/  ' e2  '@'  E  :  A ']'").
 Notation "'REL' e1 '<<' e2 ':' A" :=
-  (refines ⊤ e1%E e2%E (A)%lty2)
+  (refines ⊤ e1%E e2%E (A)%lrel)
   (at level 100, e1, e2 at next level,
    A at level 200,
    format "'[hv' 'REL'  e1  '/' '<<'  '/  ' e2  :  A ']'").
@@ -268,7 +268,7 @@ Section monadic.
     by iMod ("Hf" with "HA Hs Hj") as "Hf/=".
   Qed.
 
-  Lemma refines_ret E e1 e2 v1 v2 (A : lty2 Σ) :
+  Lemma refines_ret E e1 e2 v1 v2 (A : lrel Σ) :
     IntoVal e1 v1 →
     IntoVal e2 v2 →
     (|={E,⊤}=> A v1 v2) -∗ REL e1 << e2 @ E : A.
diff --git a/theories/logic/rules.v b/theories/logic/rules.v
index 2247bc7cfab6f6a007d54c8bd3a5628221b2b0b3..44bfb800ee6a3f8df91fb95d55663fc7188511f9 100644
--- a/theories/logic/rules.v
+++ b/theories/logic/rules.v
@@ -9,7 +9,7 @@ From reloc.prelude Require Import ctx_subst.
 
 Section rules.
   Context `{relocG Σ}.
-  Implicit Types A : lty2 Σ.
+  Implicit Types A : lrel Σ.
   Implicit Types e t : expr.
   Implicit Types v w : val.
 
@@ -262,7 +262,7 @@ Section rules.
   Qed.
 
   Lemma refines_fork e e' :
-    (REL e << e' : ()%lty2) -∗
+    (REL e << e' : ()%lrel) -∗
     REL Fork e << Fork e' : ().
   Proof.
     rewrite refines_eq /refines_def.
@@ -282,7 +282,7 @@ Section rules.
     AsRecV v' f' x' eb' →
     □(∀ v1 v2, A v1 v2 -∗
       REL App v (of_val v1) << App v' (of_val v2) : A') -∗
-    REL v << v' : (A → A')%lty2.
+    REL v << v' : (A → A')%lrel.
   Proof.
     rewrite /AsRecV. iIntros (-> ->) "#H".
     iApply refines_spec_ctx. iDestruct 1 as (ρ) "#Hs".
diff --git a/theories/proofmode.v b/theories/reloc.v
similarity index 82%
rename from theories/proofmode.v
rename to theories/reloc.v
index 6ab40a36da9bd4f2e687675606d0971a512981d9..9e4e1d3c796b590fa0204cd3d9b857958ac19edc 100644
--- a/theories/proofmode.v
+++ b/theories/reloc.v
@@ -2,3 +2,4 @@ From iris.heap_lang Require Export lang notation proofmode.
 From iris.proofmode Require Export tactics.
 From reloc.logic Require Export proofmode.tactics proofmode.spec_tactics model.
 From reloc.logic Require Export rules derived compatibility.
+From reloc.typing Require Export interp soundness.
diff --git a/theories/tests/proofmode_tests.v b/theories/tests/proofmode_tests.v
index c050c227d7a21c76e1b2c77ff8c69bfd84d18303..1adc17e8e1d5e3278c26ec082f37cbecbd2a101a 100644
--- a/theories/tests/proofmode_tests.v
+++ b/theories/tests/proofmode_tests.v
@@ -5,7 +5,7 @@ From iris.heap_lang Require Import lang notation.
 Section test.
 Context `{relocG Σ}.
 
-Definition EqI : lty2 Σ := Lty2 (λ v1 v2, ⌜v1 = v2⌝)%I.
+Definition EqI : lrel Σ := LRel (λ v1 v2, ⌜v1 = v2⌝)%I.
 (* Pure reductions *)
 Lemma test1 A P t :
   ▷ P -∗
diff --git a/theories/typing/fundamental.v b/theories/typing/fundamental.v
index 22aea120c87dae0e5294a305985b968deb9b860f..a0e99262313940a4aa0e7d412b993257163927da 100644
--- a/theories/typing/fundamental.v
+++ b/theories/typing/fundamental.v
@@ -2,7 +2,7 @@
 (** Compatibility lemmas for the logical relation *)
 From iris.heap_lang Require Import proofmode.
 From reloc.logic Require Import model.
-From reloc Require Export proofmode.
+From reloc.logic Require Export rules derived compatibility proofmode.tactics.
 From reloc.typing Require Export interp.
 
 From iris.proofmode Require Export tactics.
@@ -10,7 +10,7 @@ From Autosubst Require Import Autosubst.
 
 Section fundamental.
   Context `{relocG Σ}.
-  Implicit Types Δ : listC (lty2C Σ).
+  Implicit Types Δ : listC (lrelC Σ).
   Hint Resolve to_of_val.
 
   Local Ltac intro_clause := progress (iIntros (vs) "#Hvs /=").
@@ -132,19 +132,19 @@ Section fundamental.
   Proof.
     iIntros "IH".
     intro_clause.
-    iApply refines_fork; first solve_ndisj.
+    iApply refines_fork.
     by iApply "IH".
   Qed.
 
   Lemma bin_log_related_tlam Δ Γ (e e' : expr) τ :
-    (∀ (A : lty2 Σ),
+    (∀ (A : lrel Σ),
       □ ({(A::Δ);⤉Γ} ⊨ e ≤log≤ e' : τ)) -∗
     {Δ;Γ} ⊨ (Λ: e) ≤log≤ (Λ: e') : TForall τ.
   Proof.
     iIntros "#H".
    intro_clause.
     iApply refines_spec_ctx. iDestruct 1 as (ρ) "#Hs".
-    value_case. rewrite /lty2_forall /lty2_car /=.
+    value_case. rewrite /lrel_forall /lrel_car /=.
     iModIntro. iModIntro. iIntros (A) "!>". iIntros (? ?) "_".
     rel_pure_l. rel_pure_r.
     iDestruct ("H" $! A) as "#H1".
@@ -165,7 +165,7 @@ Section fundamental.
     by rewrite -interp_subst.
   Qed.
 
-  Lemma bin_log_related_tapp (τi : lty2 Σ) Δ Γ e e' τ :
+  Lemma bin_log_related_tapp (τi : lrel Σ) Δ Γ e e' τ :
     ({Δ;Γ} ⊨ e ≤log≤ e' : TForall τ) -∗
     {τi::Δ;⤉Γ} ⊨ (TApp e) ≤log≤ (TApp e') : τ.
   Proof.
@@ -202,7 +202,7 @@ Section fundamental.
     {Δ;Γ} ⊨ (e1;; e2) ≤log≤ (e1';; e2') : τ2.
   Proof.
     iIntros "He1 He2".
-    iApply (bin_log_related_seq lty2_true _ _ _ _ _ _ Ï„1.[ren (+1)] with "[He1] He2").
+    iApply (bin_log_related_seq lrel_true _ _ _ _ _ _ Ï„1.[ren (+1)] with "[He1] He2").
     intro_clause.
     rewrite interp_ren -(interp_ren_up [] Δ τ1).
     by iApply "He1".
@@ -422,8 +422,8 @@ Section fundamental.
     iIntros "IH".
     intro_clause.
     rel_bind_ap e e' "IH" v v' "IH".
-    iEval (rewrite lty_rec_unfold /lty2_car /=) in "IH".
-    change (lty2_rec _) with (interp (TRec τ) Δ).
+    iEval (rewrite lty_rec_unfold /lrel_car /=) in "IH".
+    change (lrel_rec _) with (interp (TRec τ) Δ).
     rel_rec_l. rel_rec_r.
     value_case. by rewrite -interp_subst.
   Qed.
@@ -437,8 +437,8 @@ Section fundamental.
     rel_bind_ap e e' "IH" v v' "IH".
     value_case.
     iModIntro.
-    iEval (rewrite lty_rec_unfold /lty2_car /=).
-    change (lty2_rec _) with (interp (TRec τ) Δ).
+    iEval (rewrite lty_rec_unfold /lrel_car /=).
+    change (lrel_rec _) with (interp (TRec τ) Δ).
     by rewrite -interp_subst.
   Qed.
 
@@ -454,7 +454,7 @@ Section fundamental.
     by rewrite interp_subst.
   Qed.
 
-  Lemma bin_log_related_pack (τi : lty2 Σ) Δ Γ e e' τ :
+  Lemma bin_log_related_pack (τi : lrel Σ) Δ Γ e e' τ :
     ({τi::Δ;⤉Γ} ⊨ e ≤log≤ e' : τ) -∗
     {Δ;Γ} ⊨ e ≤log≤ e' : TExists τ.
   Proof.
@@ -469,7 +469,7 @@ Section fundamental.
 
   Lemma bin_log_related_unpack Δ Γ x e1 e1' e2 e2' τ τ2 :
     ({Δ;Γ} ⊨ e1 ≤log≤ e1' : TExists τ) -∗
-    (∀ τi : lty2 Σ,
+    (∀ τi : lrel Σ,
       {τi::Δ;<[x:=τ]>(⤉Γ)} ⊨
         e2 ≤log≤ e2' : (subst (ren (+1)) τ2)) -∗
     {Δ;Γ} ⊨ (unpack: x := e1 in e2) ≤log≤ (unpack: x := e1' in e2') : τ2.
diff --git a/theories/typing/interp.v b/theories/typing/interp.v
index 2dca5f7db887b55a06ce2bb05d13df89ee0dbff2..9ac159cb0e161baa535442f31873a483f2e7c4d4 100644
--- a/theories/typing/interp.v
+++ b/theories/typing/interp.v
@@ -11,8 +11,8 @@ From Autosubst Require Import Autosubst.
 Section semtypes.
   Context `{relocG Σ}.
 
-  Program Definition ctx_lookup (x : var) : listC (lty2C Σ) -n> (lty2C Σ)
-    := λne Δ, (from_option id lty2_true (Δ !! x))%I.
+  Program Definition ctx_lookup (x : var) : listC (lrelC Σ) -n> (lrelC Σ)
+    := λne Δ, (from_option id lrel_true (Δ !! x))%I.
   Next Obligation.
     intros x n Δ Δ' HΔ.
     destruct (Δ !! x) as [P|] eqn:HP; cbn in *.
@@ -25,24 +25,24 @@ Section semtypes.
       rewrite HP in HP'. inversion HP'.
   Qed.
 
-  Program Fixpoint interp (τ : type) : listC (lty2C Σ) -n> lty2C Σ :=
-    match τ as _ return listC (lty2C Σ) -n> lty2C Σ with
-    | TUnit => λne _, lty2_unit
-    | TNat => λne _, lty2_int
-    | TBool => λne _, lty2_bool
-    | TProd τ1 τ2 => λne Δ, lty2_prod (interp τ1 Δ) (interp τ2 Δ)
-    | TSum τ1 τ2 => λne Δ, lty2_sum (interp τ1 Δ) (interp τ2 Δ)
-    | TArrow τ1 τ2 => λne Δ, lty2_arr (interp τ1 Δ) (interp τ2 Δ)
-    | TRec τ' => λne Δ, lty2_rec (λne τ, interp τ' (τ::Δ))
+  Program Fixpoint interp (τ : type) : listC (lrelC Σ) -n> lrelC Σ :=
+    match τ as _ return listC (lrelC Σ) -n> lrelC Σ with
+    | TUnit => λne _, lrel_unit
+    | TNat => λne _, lrel_int
+    | TBool => λne _, lrel_bool
+    | TProd τ1 τ2 => λne Δ, lrel_prod (interp τ1 Δ) (interp τ2 Δ)
+    | TSum τ1 τ2 => λne Δ, lrel_sum (interp τ1 Δ) (interp τ2 Δ)
+    | TArrow τ1 τ2 => λne Δ, lrel_arr (interp τ1 Δ) (interp τ2 Δ)
+    | TRec τ' => λne Δ, lrel_rec (λne τ, interp τ' (τ::Δ))
     | TVar x => ctx_lookup x
-    | TForall τ' => λne Δ, lty2_forall (λ τ, interp τ' (τ::Δ))
-    | TExists τ' => λne Δ, lty2_exists (λ τ, interp τ' (τ::Δ))
-    | Tref τ => λne Δ, lty2_ref (interp τ Δ)
+    | TForall τ' => λne Δ, lrel_forall (λ τ, interp τ' (τ::Δ))
+    | TExists τ' => λne Δ, lrel_exists (λ τ, interp τ' (τ::Δ))
+    | Tref τ => λne Δ, lrel_ref (interp τ Δ)
     end.
   Solve Obligations with (intros I τ τ' n Δ Δ' HΔ' ??; solve_proper).
   Next Obligation.
     intros I τ τ' n Δ Δ' HΔ' ??.
-    apply lty2_rec_ne=> X /=.
+    apply lrel_rec_ne=> X /=.
     apply I. by f_equiv.
   Defined.
 
@@ -79,17 +79,17 @@ End semtypes.
 (** ** Properties of the type inrpretation w.r.t. the substitutions *)
 Section interp_ren.
   Context `{relocG Σ}.
-  Implicit Types Δ : list (lty2 Σ).
+  Implicit Types Δ : list (lrel Σ).
 
-  (* TODO: why do I need to unfold lty2_car here? *)
-  Lemma interp_ren_up (Δ1 Δ2 : list (lty2 Σ)) τ τi :
+  (* TODO: why do I need to unfold lrel_car here? *)
+  Lemma interp_ren_up (Δ1 Δ2 : list (lrel Σ)) τ τi :
     interp τ (Δ1 ++ Δ2) ≡ interp (τ.[upn (length Δ1) (ren (+1)%nat)]) (Δ1 ++ τi :: Δ2).
   Proof.
     revert Δ1 Δ2. induction τ => Δ1 Δ2; simpl; eauto;
     try by
-      (intros ? ?; unfold lty2_car; simpl; properness; repeat f_equiv=>//).
+      (intros ? ?; unfold lrel_car; simpl; properness; repeat f_equiv=>//).
     - apply fixpoint_proper=> Ï„' w1 w2 /=.
-      unfold lty2_car. simpl.
+      unfold lrel_car. simpl.
       properness; auto. apply (IHÏ„ (_ :: _)).
     - intros v1 v2; simpl.
       rewrite iter_up. case_decide; simpl; properness.
@@ -99,11 +99,11 @@ Section interp_ren.
       assert ((length Δ1 + S (x - length Δ1) - length Δ1) = S (x - length Δ1))%nat as Hwat.
       { lia. }
       rewrite Hwat. simpl. done.
-    - intros v1 v2; unfold lty2_car; simpl;
+    - intros v1 v2; unfold lrel_car; simpl;
         simpl; properness; auto.
-      rewrite /lty2_car /=. properness; auto.
+      rewrite /lrel_car /=. properness; auto.
       apply refines_proper=> //. apply (IHÏ„ (_ :: _)).
-    - intros ??; unfold lty2_car; simpl; properness; auto. apply (IHÏ„ (_ :: _)).
+    - intros ??; unfold lrel_car; simpl; properness; auto. apply (IHÏ„ (_ :: _)).
   Qed.
 
   Lemma interp_ren A Δ (Γ : gmap string type) :
@@ -115,37 +115,37 @@ Section interp_ren.
     symmetry. apply (interp_ren_up []).
   Qed.
 
-  Lemma interp_weaken (Δ1 Π Δ2 : list (lty2 Σ)) τ :
+  Lemma interp_weaken (Δ1 Π Δ2 : list (lrel Σ)) τ :
     interp (τ.[upn (length Δ1) (ren (+ length Π))]) (Δ1 ++ Π ++ Δ2)
     ≡ interp τ (Δ1 ++ Δ2).
   Proof.
     revert Δ1 Π Δ2. induction τ=> Δ1 Π Δ2; simpl; eauto;
     try by
-      (intros ? ?; simpl; unfold lty2_car; simpl; repeat f_equiv =>//).
+      (intros ? ?; simpl; unfold lrel_car; simpl; repeat f_equiv =>//).
     - apply fixpoint_proper=> Ï„i ?? /=.
-      unfold lty2_car; simpl.
+      unfold lrel_car; simpl.
       properness; auto. apply (IHÏ„ (_ :: _)).
     - intros ??; simpl; properness; auto.
       rewrite iter_up; case_decide; properness; simpl.
       { by rewrite !lookup_app_l. }
       rewrite !lookup_app_r ;[| lia ..]. do 3 f_equiv. lia.
-    - intros ??; simpl; unfold lty2_car; simpl;
+    - intros ??; simpl; unfold lrel_car; simpl;
       properness; auto.
-      rewrite /lty2_car /=. properness; auto.
+      rewrite /lrel_car /=. properness; auto.
       apply refines_proper=> //. apply (IHÏ„ (_ :: _)).
-    - intros ??; unfold lty2_car; simpl; properness; auto.
+    - intros ??; unfold lrel_car; simpl; properness; auto.
         by apply (IHÏ„ (_ :: _)).
   Qed.
 
-  Lemma interp_subst_up (Δ1 Δ2 : list (lty2 Σ)) τ τ' :
+  Lemma interp_subst_up (Δ1 Δ2 : list (lrel Σ)) τ τ' :
     interp τ (Δ1 ++ interp τ' Δ2 :: Δ2)
     ≡ interp (τ.[upn (length Δ1) (τ' .: ids)]) (Δ1 ++ Δ2).
   Proof.
     revert Δ1 Δ2; induction τ=> Δ1 Δ2; simpl; eauto;
     try by
-      (intros ? ?; unfold lty2_car; simpl; properness; repeat f_equiv=>//).
+      (intros ? ?; unfold lrel_car; simpl; properness; repeat f_equiv=>//).
     - apply fixpoint_proper=> Ï„i ?? /=.
-      unfold lty2_car. simpl.
+      unfold lrel_car. simpl.
       properness; auto. apply (IHÏ„ (_ :: _)).
     - intros w1 w2; simpl.
       rewrite iter_up; case_decide; simpl; properness.
@@ -157,11 +157,11 @@ Section interp_ren.
         etrans; last by apply HW.
         asimpl. reflexivity. }
       rewrite !lookup_app_r; [|lia ..]. repeat f_equiv. lia.
-    - intros ??. unfold lty2_car; simpl;
+    - intros ??. unfold lrel_car; simpl;
       properness; auto.
-      rewrite /lty2_car /=. properness; auto.
+      rewrite /lrel_car /=. properness; auto.
       apply refines_proper=>//. apply (IHÏ„ (_ :: _)).
-    - intros ??; unfold lty2_car; simpl; properness; auto. apply (IHÏ„ (_ :: _)).
+    - intros ??; unfold lrel_car; simpl; properness; auto. apply (IHÏ„ (_ :: _)).
   Qed.
 
   Lemma interp_subst Δ2 τ τ' :
@@ -172,14 +172,14 @@ End interp_ren.
 (** * Interpretation of the environments *)
 Section env_typed.
   Context `{relocG Σ}.
-  Implicit Types A B : lty2 Σ.
-  Implicit Types Γ : gmap string (lty2 Σ).
+  Implicit Types A B : lrel Σ.
+  Implicit Types Γ : gmap string (lrel Σ).
 
   (** Substitution [vs] is well-typed w.r.t. [Γ] *)
-  Definition env_ltyped2 (Γ : gmap string (lty2 Σ))
+  Definition env_ltyped2 (Γ : gmap string (lrel Σ))
     (vs : gmap string (val*val)) : iProp Σ :=
     (⌜ ∀ x, is_Some (Γ !! x) ↔ is_Some (vs !! x) ⌝ ∧
-    [∗ map] i ↦ Avv ∈ map_zip Γ vs, lty2_car Avv.1 Avv.2.1 Avv.2.2)%I.
+    [∗ map] i ↦ Avv ∈ map_zip Γ vs, lrel_car Avv.1 Avv.2.1 Avv.2.2)%I.
 
   Notation "⟦ Γ ⟧*" := (env_ltyped2 Γ).
 
@@ -253,7 +253,7 @@ Section bin_log_related.
   Context `{relocG Σ}.
 
   Definition bin_log_related (E : coPset)
-             (Δ : list (lty2 Σ)) (Γ : stringmap type)
+             (Δ : list (lrel Σ)) (Γ : stringmap type)
              (e e' : expr) (τ : type) : iProp Σ :=
     (∀ vs, ⟦ (λ τ, interp τ Δ) <$> Γ ⟧* vs -∗
            REL (subst_map (fst <$> vs) e)