diff --git a/theories/examples/bit.v b/theories/examples/bit.v
index a9c365781a25bf34e835424d777089231881f8e4..36bc9704abe7039f232735aa3d9f097e9b8b9373 100644
--- a/theories/examples/bit.v
+++ b/theories/examples/bit.v
@@ -1,7 +1,6 @@
 From iris.proofmode Require Import tactics.
 From reloc Require Import reloc.
-From reloc.typing Require Import types interp fundamental.
-From reloc.typing Require Import soundness.
+Set Default Proof Using "Type".
 
 (* TODO: these modules should be values -- but we don't have refines_pair for values *)
 Definition bit_bool : expr :=
@@ -60,28 +59,6 @@ End bit_refinement.
 Theorem bit_ctx_refinement :
   ∅ ⊨ bit_bool ≤ctx≤ bit_nat : bitτ.
 Proof.
-  eapply (logrel_ctxequiv relocΣ).
-  iIntros (? ? vs) "Hvs". simpl.
-  (* TODO: this is not the place to have this boilerplate *)
-  rewrite !lookup_delete.
-  iApply (bit_refinement Δ).
+  eapply (refines_sound relocΣ).
+  iIntros (? Δ). iApply (bit_refinement Δ).
 Qed.
-
-(* Definition heapify : val := λ: "b", Unpack "b" $ λ: "b'", *)
-(*   let: "init" := Fst (Fst "b'") in *)
-(*   let: "flip" := Snd (Fst "b'") in *)
-(*   let: "view" := Snd "b'" in *)
-(*   let: "x" := ref "init" in *)
-(*   let: "l" := newlock #() in *)
-(*   let: "flip_ref" := λ: <>, acquire "l";; "x" <- "flip" (!"x");; release "l" in *)
-(*   let: "view_ref" := λ: <>, "view" (!"x") in *)
-(*   (#(), "flip_ref", "view_ref"). *)
-
-(* Lemma heapify_type Γ : *)
-(*   typed Γ heapify (TArrow bitτ bitτ). *)
-(* Proof. *)
-(*   unfold bitτ. unfold heapify. *)
-(*   unlock. *)
-(*   repeat (econstructor; solve_typed). (* TODO: solve_typed does not work by itself :( *) *)
-(* Qed. *)
-(* Hint Resolve heapify_type : typeable. *)
diff --git a/theories/examples/generative.v b/theories/examples/generative.v
index 0befa62fb913c7a1b3293a608c749b8ba7679e6a..fd43f80f99612f51c995a97fdc3bde05df846912 100644
--- a/theories/examples/generative.v
+++ b/theories/examples/generative.v
@@ -1,13 +1,10 @@
 (* ReLoC -- Relational logic for fine-grained concurrency *)
 (** Examples from "State-Dependent Represenation Independence" by A.
 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 reloc prelude.bijections.
+From reloc Require Export reloc.
+From reloc.prelude Require Import bijections.
 From reloc.lib Require Export counter lock.
-From reloc.typing Require Export interp soundness.
 
 (** Using references for name generation *)
 (* ∃ α. (1 → α) × (α → α → 2)                     *)
@@ -27,7 +24,7 @@ Definition nameGen2 : expr :=
   ,λ: "y" "z", "y" = "z").
 
 Section namegen_refinement.
-  Context `{relocG Σ, PrePBijG loc nat Σ}.
+  Context `{!relocG Σ, !pBijPreG loc nat Σ}.
 
   Program Definition ngR (γ : gname) : lrel Σ := LRel (λ v1 v2,
    ∃ (l : loc) (n : nat), ⌜v1 = #l%V⌝ ∗ ⌜v2 = #n⌝
@@ -76,14 +73,14 @@ Section namegen_refinement.
       iMod (bij_alloc_alt _ _ γ _ l' (S n) with "HB") as "[HB #Hl'n]"; auto.
       iMod ("Hcl" with "[-]").
       { iNext.
-        replace (Z.of_nat n + 1) with (Z.of_nat (n + 1)); last lia.
+        replace (Z.of_nat n + 1)%Z with (Z.of_nat (n + 1)); last lia.
         iExists _,_; iFrame "Hc HB".
         rewrite big_sepS_insert; last by naive_solver.
         iFrame. iSplit; first (iPureIntro; lia).
         iApply (big_sepS_mono _ _ L with "HL").
         intros [l x] Hlx. apply bi.sep_mono_r, bi.pure_mono. lia. }
       rel_values. iModIntro.
-      replace (Z.of_nat n + 1) with (Z.of_nat (S n)); last lia.
+      replace (Z.of_nat n + 1)%Z with (Z.of_nat (S n)); last lia.
       iExists l', (S n)%nat; eauto.
     - (* Name comparison *)
       rel_pure_l. rel_pure_r.
@@ -114,6 +111,16 @@ Section namegen_refinement.
   Qed.
 End namegen_refinement.
 
+Lemma nameGen_ctx_refinement :
+  ∅ ⊨ nameGen1 ≤ctx≤ nameGen2 : nameGenTy.
+Proof.
+  pose (Σ := #[relocΣ;pBijΣ loc nat]).
+  eapply (refines_sound Σ).
+  iIntros (? Δ).
+  iApply nameGen_ref1.
+Qed.
+
+
 (** A type of cells -- basically an abstract type of references. *)
 (* ∀ α, ∃ β, (α → β) × (β → α) × (β → α → ())  *)
 Definition cellτ : type :=
@@ -250,3 +257,11 @@ Section cell_refinement.
     Qed.
 End cell_refinement.
 
+Lemma cell_ctx_refinement :
+  ∅ ⊨ cell2 ≤ctx≤ cell1 : cellτ.
+Proof.
+  pose (Σ := #[relocΣ;lockΣ]).
+  eapply (refines_sound Σ).
+  iIntros (? Δ).
+  iApply cell2_cell1_refinement.
+Qed.
diff --git a/theories/examples/or.v b/theories/examples/or.v
index ff88965897d5c788656d1f74ada50e79659b2c1f..5f86bbe9a6fac403354c130bcaf4c7df82f7930a 100644
--- a/theories/examples/or.v
+++ b/theories/examples/or.v
@@ -1,8 +1,7 @@
 (* ReLoC -- Relational logic for fine-grained concurrency *)
 (** (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 reloc lib.Y (* for bot *).
+Set Default Proof Using "Type".
 
 (** (Binary) non-determinism can be simluated with concurrency. In
 this file we derive the algebraic laws for parallel "or"/demonic
@@ -196,3 +195,4 @@ Section rules.
 
 End rules.
 
+(* TODO: write out the contextual refinements *)
diff --git a/theories/examples/symbol.v b/theories/examples/symbol.v
index 685b1f055730dbcde9a3c6cfd152be558b39053b..9957ce7f722ecb93e0195e42cbce9b619c957349 100644
--- a/theories/examples/symbol.v
+++ b/theories/examples/symbol.v
@@ -6,13 +6,12 @@ In this example we implement a symbol lookup table, where a symbol is
 an abstract data type. Because the only way to obtain a symbol is to
 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 reloc.
 From reloc.lib Require Import lock list.
 
 (** * Symbol table *)
-Definition lty_symbol `{relocG Σ} : lrel Σ :=
+Definition lrel_symbol `{relocG Σ} : lrel Σ :=
   ∃ α, (α → α → lrel_bool)    (* equality check *)
      * (lrel_int → α)          (* insert *)
      * (α → lrel_int).         (* lookup *)
@@ -50,7 +49,7 @@ Definition symbol2 : val := λ: <>,
 Class msizeG Σ := MSizeG { msize_inG :> inG Σ (authR mnatUR) }.
 Definition msizeΣ : gFunctors := #[GFunctor (authR mnatUR)].
 
-Instance subG_mcounterΣ {Σ} : subG msizeΣ Σ → msizeG Σ.
+Instance subG_msizeΣ {Σ} : subG msizeΣ Σ → msizeG Σ.
 Proof. solve_inG. Qed.
 
 Section rules.
@@ -106,7 +105,7 @@ Section rules.
     (∃ (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 lrel_int ls ls)%I.
+                           ∗ lrel_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
@@ -217,18 +216,11 @@ Section proof.
     - rel_values.
   Qed.
 
-  Definition symbolτ : type :=
-    TExists (TProd (TProd (TArrow (TVar 0) (TArrow (TVar 0) TBool))
-                          (TArrow TNat (TVar 0)))
-                   (TArrow (TVar 0) TNat))%nat.
-  Lemma refinement1 Δ :
-    {Δ;∅} ⊨ symbol1 ≤log≤ symbol2 : TArrow TUnit symbolτ.
+  Lemma refinement1 :
+    REL symbol1 << symbol2 : () → lrel_symbol.
   Proof.
     unlock symbol1 symbol2.
-    iIntros (vs) "Hvs". rewrite fmap_empty.
-    rewrite env_ltyped2_empty_inv. iDestruct "Hvs" as %->.
-    rewrite !fmap_empty !subst_map_empty.
-    iApply refines_arrow_val. fold interp.
+    iApply refines_arrow_val.
     iAlways. iIntros (? ?) "[% %]"; simplify_eq/=.
     rel_let_l. rel_let_r.
     rel_alloc_l size1 as "[Hs1 Hs1']"; repeat rel_pure_l.
@@ -237,7 +229,7 @@ Section proof.
     rel_alloc_r tbl2 as "[Htbl2 Htbl2']"; repeat rel_pure_r.
     iMod (own_alloc (● (0%nat : mnat))) as (γ) "Ha"; first done.
     iMod (inv_alloc sizeN _ (table_inv γ size1 size2 tbl1 tbl2) with "[Hs1 Hs2 Htbl1 Htbl2 Ha]") as "#Hinv".
-    { iNext. iExists _,_. iFrame. iApply lty_list_nil. }
+    { iNext. iExists _,_. iFrame. iApply lrel_list_nil. }
     rel_apply_r refines_newlock_r.
     iIntros (l2) "Hl2". rel_pure_r. rel_pure_r.
     pose (N:=(relocN.@"lock1")).
@@ -293,7 +285,7 @@ Section proof.
       iDestruct "Htbl2" as "[Htbl2 Htbl2']".
       iMod ("Hcl" with "[Ha Hs1 Hs2 Htbl1 Htbl2]") as "_".
       { iNext. iExists _,_. iFrame.
-        iApply lty_list_cons; eauto. }
+        iApply lrel_list_cons; eauto. }
       rel_apply_l (refines_release_l with "Hl1 Hlk [-]"); auto.
       { iExists _,_. by iFrame. }
       iNext. do 2 rel_pure_l. rel_values.
@@ -304,14 +296,11 @@ Section proof.
       unlock. iApply "H". (* TODO how to avoid this? *)
   Qed.
 
-  Lemma refinement2 Δ :
-    {Δ;∅} ⊨ symbol2 ≤log≤ symbol1 : TArrow TUnit symbolτ.
+  Lemma refinement2 :
+    REL symbol2 << symbol1 : () → lrel_symbol.
   Proof.
     unlock symbol1 symbol2.
-    iIntros (vs) "Hvs". rewrite fmap_empty.
-    rewrite env_ltyped2_empty_inv. iDestruct "Hvs" as %->.
-    rewrite !fmap_empty !subst_map_empty.
-    iApply refines_arrow_val. fold interp.
+    iApply refines_arrow_val.
     iAlways. iIntros (? ?) "[% %]"; simplify_eq/=.
     rel_let_l. rel_let_r.
     rel_alloc_l size1 as "[Hs1 Hs1']"; repeat rel_pure_l.
@@ -320,7 +309,7 @@ Section proof.
     rel_alloc_r tbl2 as "[Htbl2 Htbl2']"; repeat rel_pure_r.
     iMod (own_alloc (● (0%nat : mnat))) as (γ) "Ha"; first done.
     iMod (inv_alloc sizeN _ (table_inv γ size1 size2 tbl1 tbl2) with "[Hs1 Hs2 Htbl1 Htbl2 Ha]") as "#Hinv".
-    { iNext. iExists _,_. iFrame. iApply lty_list_nil. }
+    { iNext. iExists _,_. iFrame. iApply lrel_list_nil. }
     rel_apply_r refines_newlock_r.
     iIntros (l2) "Hl2". rel_pure_r. rel_pure_r.
     pose (N:=(relocN.@"lock1")).
@@ -376,7 +365,7 @@ Section proof.
       iDestruct "Htbl2" as "[Htbl2 Htbl2']".
       iMod ("Hcl" with "[Ha Hs1 Hs2 Htbl1 Htbl2]") as "_".
       { iNext. iExists _,_. iFrame.
-        iApply lty_list_cons; eauto. }
+        iApply lrel_list_cons; eauto. }
       rel_apply_l (refines_release_l with "Hl1 Hlk [-]"); auto.
       { iExists _,_. by iFrame. }
       iNext. do 2 rel_pure_l. rel_values.
@@ -387,3 +376,25 @@ Section proof.
       unlock. iApply "H". (* TODO how to avoid this? *)
   Qed.
 End proof.
+
+Definition symbolτ : type :=
+  TExists (TProd (TProd (TArrow (TVar 0) (TArrow (TVar 0) TBool))
+                        (TArrow TNat (TVar 0)))
+                        (TArrow (TVar 0) TNat))%nat.
+
+Theorem symbol_ctx_refinement1 :
+  ∅ ⊨ symbol1 ≤ctx≤ symbol2 :
+    TArrow TUnit symbolτ.
+Proof.
+  pose (Σ := #[relocΣ;msizeΣ;lockΣ]).
+  eapply (refines_sound Σ).
+  iIntros (? Δ). iApply refinement1.
+Qed.
+
+Theorem symbol_ctx_refinement2 :
+  ∅ ⊨ symbol2 ≤ctx≤ symbol1 : TArrow TUnit symbolτ.
+Proof.
+  pose (Σ := #[relocΣ;msizeΣ;lockΣ]).
+  eapply (refines_sound Σ).
+  iIntros (? Δ). iApply refinement2.
+Qed.
diff --git a/theories/examples/ticket_lock.v b/theories/examples/ticket_lock.v
index 129a021e62e0fa17782c7d90d1515f4d5341a879..27b50731ea8fb60ffe786d6a663ace066ddb2144 100644
--- a/theories/examples/ticket_lock.v
+++ b/theories/examples/ticket_lock.v
@@ -24,14 +24,20 @@ Class tlockG Σ :=
   tlock_G :> authG Σ (gset_disjUR nat).
 Definition tlockΣ : gFunctors :=
   #[ authΣ (gset_disjUR nat) ].
+Instance subG_tlockΣ {Σ} : subG tlockΣ Σ → tlockG Σ.
+Proof. solve_inG. Qed.
 
 Definition lockPool := gset ((loc * loc * gname) * loc).
 Definition lockPoolR := gsetUR ((loc * loc * gname) * loc).
 
 Class lockPoolG Σ :=
   lockPool_inG :> authG Σ lockPoolR.
+Definition lockPoolΣ := #[ authΣ lockPoolR ].
+Instance subG_lockPoolΣ {Σ} : subG lockPoolΣ Σ → lockPoolG Σ.
+Proof. solve_inG. Qed.
+
 Section refinement.
-  Context `{relocG Σ, tlockG Σ, lockPoolG Σ}.
+  Context `{!relocG Σ, !tlockG Σ, !lockPoolG Σ}.
 
   (** * Basic abstractions around the concrete RA *)
 
@@ -362,3 +368,13 @@ Section refinement.
   Qed.
 
 End refinement.
+
+Lemma ticket_lock_ctx_refinement :
+  ∅ ⊨   (newlock, acquire, release)
+  ≤ctx≤ (reloc.lib.lock.newlock, reloc.lib.lock.acquire, reloc.lib.lock.release)
+  : lockT.
+Proof.
+  pose (Σ := #[relocΣ;tlockΣ;lockPoolΣ]).
+  eapply (refines_sound Σ).
+  iIntros (? Δ). iApply (ticket_lock_refinement Δ).
+Qed.
diff --git a/theories/lib/Y.v b/theories/lib/Y.v
index be43aaa921a3c527cc3ddf06bd84243640dd93b6..e00da894dfb852e7fbf2a603e4f1ac7f4b036af1 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 reloc.
+Set Default Proof Using "Type".
 
 Definition bot : val := rec: "bot" <> := "bot" #().
 
diff --git a/theories/lib/assert.v b/theories/lib/assert.v
index 930db3385ec0ebdc66eb76c6ccc22c2697822f8a..e95364c94bb4b1365c302ea656b61268e9b2a49b 100644
--- a/theories/lib/assert.v
+++ b/theories/lib/assert.v
@@ -1,7 +1,5 @@
-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 reloc.
+From iris.heap_lang.lib Require Export assert.
 Set Default Proof Using "Type".
 
 Definition assert : val :=
diff --git a/theories/lib/counter.v b/theories/lib/counter.v
index ad9536a26a5dcc31eb8d8abc84c6aaf2fb371ee7..0ab62f09a6ec5cec37555c9a44eababb7eaa5908 100644
--- a/theories/lib/counter.v
+++ b/theories/lib/counter.v
@@ -1,8 +1,6 @@
 From reloc Require Export reloc.
-From reloc.typing Require Export types interp.
-From reloc.logic Require Import compatibility.
 From reloc.lib Require Import lock.
-From reloc.typing Require Import soundness.
+Set Default Proof Using "Type".
 
 Definition CG_increment : val := λ: "x" "l",
   acquire "l";;
@@ -230,7 +228,6 @@ Theorem counter_ctx_refinement :
   ∅ ⊨ FG_counter ≤ctx≤ CG_counter :
          TArrow TUnit (TProd (TArrow TUnit TNat) (TArrow TUnit TNat)).
 Proof.
-  eapply (logrel_ctxequiv relocΣ).
-  iIntros (? Δ vs) "#Hvs".
-  iApply FG_CG_counter_refinement.
+  eapply (refines_sound relocΣ).
+  iIntros (? Δ). iApply FG_CG_counter_refinement.
 Qed.
diff --git a/theories/lib/list.v b/theories/lib/list.v
index 77c8e5585d05d2ff0119a21444b889682b4006b4..72f7f4d8c10a0b54b9b494b894edeea56dea1595 100644
--- a/theories/lib/list.v
+++ b/theories/lib/list.v
@@ -1,7 +1,7 @@
 (* ReLoC -- Relational logic for fine-grained concurrency *)
 (** Lists, their semantics types, and operations on them *)
 From reloc Require Import reloc.
-From reloc.typing Require Import types interp.
+Set Default Proof Using "Type".
 
 Notation CONS h t := (SOME (Pair h t)).
 Notation CONSV h t := (SOMEV (PairV h t)).
@@ -14,7 +14,7 @@ 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 : lrel Σ) : lrel Σ :=
+Program Definition lrel_list `{relocG Σ} (A : lrel Σ) : lrel Σ :=
   lrel_rec (λne B, () + (A * B))%lrel.
 Next Obligation. solve_proper. Qed.
 
@@ -26,23 +26,23 @@ Definition nth : val := rec: "nth" "l" "n" :=
                  else "nth" (Snd "xs") ("n" - #1)
   end.
 
-Lemma lty_list_nil `{relocG Σ} A :
-  lty_list A NILV NILV.
+Lemma lrel_list_nil `{relocG Σ} A :
+  lrel_list A NILV NILV.
 Proof.
-  unfold lty_list.
-  rewrite lty_rec_unfold /=.
+  unfold lrel_list.
+  rewrite lrel_rec_unfold /=.
   unfold lrel_rec1 , lrel_car. (* TODO so much unfolding *)
   simpl. iNext.
   iExists _,_. iLeft. repeat iSplit; eauto.
 Qed.
 
-Lemma lty_list_cons `{relocG Σ} (A : lrel Σ) v1 v2 ls1 ls2 :
+Lemma lrel_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).
+  lrel_list A ls1 ls2 -∗
+  lrel_list A (CONSV v1 ls1) (CONSV v2 ls2).
 Proof.
   iIntros "#HA #Hls".
-  rewrite {2}/lty_list lty_rec_unfold /=.
+  rewrite {2}/lrel_list lrel_rec_unfold /=.
   rewrite /lrel_rec1 {3}/lrel_car.
   iNext. simpl. iExists _, _.
   iRight. repeat iSplit; eauto.
@@ -95,5 +95,5 @@ Proof.
 Qed.
 
 Lemma nth_int_typed `{relocG Σ} :
-  REL nth << nth : lty_list lrel_int → lrel_int → lrel_int.
+  REL nth << nth : lrel_list lrel_int → lrel_int → lrel_int.
 Proof. admit. Admitted.
diff --git a/theories/lib/lock.v b/theories/lib/lock.v
index 8b5a31bd5886dbe692bdf050d4f34da14a548193..26ba9dfe5c3db72b640141f23fd7e7209d3597dd 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 reloc.
+From iris.algebra Require Import excl.
+Set Default Proof Using "Type".
 
 Definition newlock : val := λ: <>, ref #false.
 Definition acquire : val := rec: "acquire" "x" :=
diff --git a/theories/logic/model.v b/theories/logic/model.v
index 1be0b07cb524440fa2f71e5cc8103de5190168d8..2d472e7887ea58df83aca34636ac08598fcbf19a 100644
--- a/theories/logic/model.v
+++ b/theories/logic/model.v
@@ -18,8 +18,8 @@ Record lrel Σ := LRel {
 }.
 Arguments LRel {_} _%I {_}.
 Arguments lrel_car {_} _ _ _ : simpl never.
-Bind Scope lty_scope with lrel.
-Delimit Scope lty_scope with lrel.
+Bind Scope lrel_scope with lrel.
+Delimit Scope lrel_scope with lrel.
 Existing Instance lrel_persistent.
 
 (* The COFE structure on semantic types *)
@@ -139,21 +139,21 @@ Section semtypes.
     apply lrel_car_ne; eauto.
   Qed.
 
-  Lemma lty_rec_unfold (C : lrelC Σ -n> lrelC Σ) : lrel_rec C ≡ lrel_rec1 C (lrel_rec C).
+  Lemma lrel_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 "()" := 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 "()" := lrel_unit : lrel_scope.
+Infix "→" := lrel_arr : lrel_scope.
+Infix "*" := lrel_prod : lrel_scope.
+Infix "+" := lrel_sum : lrel_scope.
+Notation "'ref' A" := (lrel_ref A) : lrel_scope.
 Notation "∃ A1 .. An , C" :=
-  (lrel_exists (λ A1, .. (lrel_exists (λ An, C%lrel)) ..)) : lty_scope.
+  (lrel_exists (λ A1, .. (lrel_exists (λ An, C%lrel)) ..)) : lrel_scope.
 Notation "∀ A1 .. An , C" :=
-  (lrel_forall (λ A1, .. (lrel_forall (λ An, C%lrel)) ..)) : lty_scope.
+  (lrel_forall (λ A1, .. (lrel_forall (λ An, C%lrel)) ..)) : lrel_scope.
 
 Section semtypes_properties.
   Context `{relocG Σ}.
diff --git a/theories/prelude/bijections.v b/theories/prelude/bijections.v
index a040be21fdd01ef1e1cbe240ee69b053dd452eae..cfe7174f006effaf95fb1b9871f93a7924b34def 100644
--- a/theories/prelude/bijections.v
+++ b/theories/prelude/bijections.v
@@ -43,14 +43,17 @@ Proof.
 Qed.
 
 Definition bijUR := gsetUR (A * B).
-Class PrePBijG Σ := prePBijG
-{ prePBijG_inG :> authG Σ bijUR }.
-Class PBijG Σ := pBijG
-{ PBijG_inG :> authG Σ bijUR
-; PBijG_name : gname }.
+Class pBijPreG Σ := PBijPreG
+{ pBijPreG_inG :> authG Σ bijUR }.
+Class pBijG Σ := PBijG
+{ pBijG_inG :> authG Σ bijUR
+; pBijG_name : gname }.
+Definition pBijΣ : gFunctors := #[ authΣ bijUR ].
+Global Instance subG_pBijΣ {Σ} : subG pBijΣ Σ → pBijPreG Σ.
+Proof. solve_inG. Qed.
 
 Section logic.
-  Context `{PrePBijG Σ}.
+  Context `{pBijPreG Σ}.
 
   Definition BIJ_def γ (L : bijUR) : iProp Σ :=
     (own γ (● L) ∗ ⌜bijective L⌝)%I.
diff --git a/theories/typing/fundamental.v b/theories/typing/fundamental.v
index a0e99262313940a4aa0e7d412b993257163927da..c394641f6d0dda35d3b658d5c542730fb7338748 100644
--- a/theories/typing/fundamental.v
+++ b/theories/typing/fundamental.v
@@ -422,7 +422,7 @@ Section fundamental.
     iIntros "IH".
     intro_clause.
     rel_bind_ap e e' "IH" v v' "IH".
-    iEval (rewrite lty_rec_unfold /lrel_car /=) in "IH".
+    iEval (rewrite lrel_rec_unfold /lrel_car /=) in "IH".
     change (lrel_rec _) with (interp (TRec τ) Δ).
     rel_rec_l. rel_rec_r.
     value_case. by rewrite -interp_subst.
@@ -437,7 +437,7 @@ Section fundamental.
     rel_bind_ap e e' "IH" v v' "IH".
     value_case.
     iModIntro.
-    iEval (rewrite lty_rec_unfold /lrel_car /=).
+    iEval (rewrite lrel_rec_unfold /lrel_car /=).
     change (lrel_rec _) with (interp (TRec τ) Δ).
     by rewrite -interp_subst.
   Qed.
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index 94d931e303211b62f07623d34822ba1f2d42971a..e22a0b8870dff1781aa501a2f170ff2fb08694b6 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -68,3 +68,15 @@ Proof.
   iApply (bin_log_related_under_typed_ctx with "[]"); eauto.
   iAlways. iIntros (?). iApply Hlog.
 Qed.
+
+Lemma refines_sound Σ `{relocPreG Σ} e e' τ :
+  (∀ `{relocG Σ} Δ, REL e << e' : (interp τ Δ)) →
+  ∅ ⊨ e ≤ctx≤ e' : τ.
+Proof.
+  intros Hlog. eapply logrel_ctxequiv. apply _.
+  iIntros (? Δ vs).
+  rewrite fmap_empty env_ltyped2_empty_inv.
+  iIntros (->).
+  rewrite !fmap_empty !subst_map_empty.
+  iApply Hlog.
+Qed.