diff --git a/theories/examples/bit.v b/theories/examples/bit.v
index 0ca7c8b8758368af40f579e85216c7102c9d00b3..d3c714b902bce109fadcf958c65a91abb602fb1b 100644
--- a/theories/examples/bit.v
+++ b/theories/examples/bit.v
@@ -1,3 +1,5 @@
+(* ReLoC -- Relational logic for fine-grained concurrency *)
+(** A simple bit module *)
 From iris.proofmode Require Import tactics.
 From reloc Require Import reloc.
 Set Default Proof Using "Type".
diff --git a/theories/examples/cell.v b/theories/examples/cell.v
index 950614302c9f7e36a5c8a9141dd6cbe699eb5c80..c7e4ba8c805d350b872cc9ad3f89be5f64894bdd 100644
--- a/theories/examples/cell.v
+++ b/theories/examples/cell.v
@@ -59,22 +59,10 @@ Section cell_refinement.
   Lemma cell2_cell1_refinement :
     REL cell2 << cell1 : ∀ α, ∃ β, (α → β) * (β → α) * (β → α → ()).
   Proof.
-    (* TODO: this uuugly *)
-    pose (Ï„ := (TExists (TProd (TProd (TArrow (TVar 1) (TVar 0))
-                                 (TArrow (TVar 0) (TVar 1)))
-                                 (TArrow (TVar 0) (TArrow (TVar 1) TUnit))))%nat).
-    iPoseProof (bin_log_related_tlam [] ∅ _ _ τ) as "H".
-    iSpecialize ("H" with "[]"); last first.
-    { rewrite /bin_log_related.
-      iSpecialize ("H" $! ∅ with "[]").
-      - rewrite fmap_empty. iApply env_ltyped2_empty.
-      - rewrite !fmap_empty !subst_map_empty.
-        iSimpl in "H". iApply "H". }
-    iIntros (R) "!#".
-    iApply (bin_log_related_pack (cellR R)).
-    iIntros (vs) "Hvs". rewrite !fmap_empty env_ltyped2_empty_inv.
-    iDestruct "Hvs" as %->. rewrite !fmap_empty !subst_map_empty.
-    iSimpl. repeat iApply refines_pair.
+    unfold cell1, cell2. rel_pure_l. rel_pure_r.
+    iApply refines_forall. iAlways. iIntros (R).
+    iApply (refines_exists (cellR R)).
+    repeat iApply refines_pair.
     - (* New cell *)
       rel_pure_l. rel_pure_r.
       iApply refines_arrow_val.
diff --git a/theories/logic/compatibility.v b/theories/logic/compatibility.v
index 3ed171b7252abd4cc47d3c64f080621a4cc2516e..c6f767362b23d1f010ea35e1a8eb9f3ac304a5ff 100644
--- a/theories/logic/compatibility.v
+++ b/theories/logic/compatibility.v
@@ -68,5 +68,15 @@ Section compatibility.
     iModIntro. iExists A. done.
   Qed.
 
+  Lemma refines_forall e e' (C : lrel Σ → lrel Σ) :
+    □ (∀ A, REL e << e' : C A) -∗
+    REL (λ: <>, e)%V << (λ: <>, e')%V : ∀ A, C A.
+  Proof.
+    iIntros "#H".
+    rel_values. iModIntro.
+    iIntros (A ? ?) "_ !#".
+    rel_rec_l. rel_rec_r. iApply "H".
+  Qed.
+
 End compatibility.
 
diff --git a/theories/logic/model.v b/theories/logic/model.v
index 2d472e7887ea58df83aca34636ac08598fcbf19a..6a4fa17d0a7a98a83aa3214ad2c42f7449560ba1 100644
--- a/theories/logic/model.v
+++ b/theories/logic/model.v
@@ -114,7 +114,7 @@ Section semtypes.
     ∃ A, C A 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.
+    ∀ A : lrel Σ, (lrel_arr lrel_unit (C A))%lrel w1 w2)%I.
 
   Definition lrel_true : lrel Σ := LRel (λ w1 w2, True)%I.
 
diff --git a/theories/typing/fundamental.v b/theories/typing/fundamental.v
index c394641f6d0dda35d3b658d5c542730fb7338748..a47064b297fae91d2120557ca449f2338d5e075a 100644
--- a/theories/typing/fundamental.v
+++ b/theories/typing/fundamental.v
@@ -142,11 +142,9 @@ Section fundamental.
     {Δ;Γ} ⊨ (Λ: e) ≤log≤ (Λ: e') : TForall τ.
   Proof.
     iIntros "#H".
-   intro_clause.
-    iApply refines_spec_ctx. iDestruct 1 as (ρ) "#Hs".
-    value_case. rewrite /lrel_forall /lrel_car /=.
-    iModIntro. iModIntro. iIntros (A) "!>". iIntros (? ?) "_".
-    rel_pure_l. rel_pure_r.
+    intro_clause. rel_pure_l. rel_pure_r.
+    iApply refines_forall.
+    iModIntro. iIntros (A).
     iDestruct ("H" $! A) as "#H1".
     iApply "H1".
     by rewrite (interp_ren A Δ Γ).
diff --git a/theories/typing/types.v b/theories/typing/types.v
index a4b524cd74cf5935e637027fce70a6ce43039ace..8b06755da94934f7a4bb93d638253d95243bd018 100644
--- a/theories/typing/types.v
+++ b/theories/typing/types.v
@@ -78,8 +78,9 @@ Reserved Notation "Γ ⊢ₜ e : τ" (at level 74, e, τ at next level).
 Notation "⤉ Γ" := (Autosubst_Classes.subst (ren (+1)%nat) <$> Γ) (at level 10, format "⤉ Γ").
 
 (** We model type-level lambdas and applications as thunks *)
-Notation "Λ: e" := (λ: <>, e)%E (at level 200).
-Notation "'TApp' e" := (App e%E #()%E) (at level 200).
+Notation "Λ: e" := (λ: <>, e)%E (at level 200, only parsing).
+Notation "Λ: e" := (λ: <>, e)%V (at level 200, only parsing) : val_scope.
+Notation "'TApp' e" := (App e%E #()%E) (at level 200, only parsing).
 
 (* To unfold a recursive type, we need to take a step. We thus define the
 unfold operator to be the identity function. *)