diff --git a/theories/logic/compatibility.v b/theories/logic/compatibility.v
index e7b2bfdc49e8ff09684c88cdf282e7e132194d45..57e11a9a0626cb0ff3ee4fbd59dea0da137f4d68 100644
--- a/theories/logic/compatibility.v
+++ b/theories/logic/compatibility.v
@@ -39,7 +39,7 @@ Section compatibility.
     iIntros "IH1 IH2".
     rel_bind_ap e2 e2' "IH2" v v' "Hvv".
     rel_bind_ap e1 e1' "IH1" f f' "Hff".
-    rewrite interp_val_arrow. by iApply "Hff".
+    by iApply "Hff".
   Qed.
 
   Lemma refines_fork e e' E :
@@ -51,7 +51,7 @@ Section compatibility.
     rewrite refines_eq /refines_def.
     iIntros (ρ) "#Hρ"; iIntros (j K) "Hj /=".
     tp_fork j as i "Hi".
-    iSpecialize ("IH" with "Hρ"). unfold interp_expr.
+    iSpecialize ("IH" with "Hρ").
     iMod ("IH" $! i [] with "Hi") as "IH".
     iApply (wp_fork with "[-Hj]").
     - iNext. iApply (wp_wand with "IH"). eauto.
diff --git a/theories/logic/model.v b/theories/logic/model.v
index 608098c3353c4aeb21ea4eb4fd79a5c62dc69c44..843a06759a0c79921a24d3c177bad7dc54259271 100644
--- a/theories/logic/model.v
+++ b/theories/logic/model.v
@@ -59,24 +59,31 @@ Section semtypes.
   Implicit Types E : coPset.
   Implicit Types A B : lty2 Σ.
 
-  Definition interp_expr E e e' A : iProp Σ :=
-    (∀ j K, j ⤇ fill K e'
-    ={E,⊤}=∗ WP e {{ v, ∃ v', j ⤇ fill K (of_val v') ∗ A v v' }})%I.
+  Definition refines_def (E : coPset)
+           (e e' : expr) (A : lty2 Σ) : 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.
 
-  Global Instance interp_expr_ne E n :
-    Proper ((=) ==> (=) ==> dist n ==> dist n) (interp_expr E).
-  Proof. solve_proper. Qed.
+  Definition refines_aux : seal refines_def. Proof. by eexists. Qed.
+  Definition refines := unseal refines_aux.
+  Definition refines_eq : refines = refines_def :=
+    seal_eq refines_aux.
+
+  Global Instance refines_ne E n :
+    Proper ((=) ==> (=) ==> (dist n) ==> (dist n)) (refines E).
+  Proof. rewrite refines_eq /refines_def. solve_proper. Qed.
 
-  Global Instance interp_expr_proper E e e' :
-    Proper ((≡) ==> (≡)) (interp_expr E e e').
-  Proof. apply ne_proper=>n. apply _. Qed.
+  Global Instance refines_proper E  :
+    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 lty2_arr (A1 A2 : lty2 Σ) : lty2 Σ := Lty2 (λ w1 w2,
-    □ ∀ v1 v2, A1 v1 v2 -∗ interp_expr ⊤ (App w1 v1) (App w2 v2) A2)%I.
+    □ ∀ v1 v2, A1 v1 v2 -∗ refines ⊤ (App w1 v1) (App w2 v2) A2)%I.
 
   Definition lty2_ref (A : lty2 Σ) : lty2 Σ := Lty2 (λ w1 w2,
     ∃ l1 l2: loc, ⌜w1 = #l1⌝ ∧ ⌜w2 = #l2⌝ ∧
@@ -107,17 +114,17 @@ Section semtypes.
     ∃ A, C A w1 w2)%I.
 
   (** The lty2 constructors are non-expansive *)
-  Instance lty2_prod_ne n : Proper (dist n ==> (dist n ==> dist n)) lty2_prod.
+  Instance lty2_prod_ne n : Proper (dist n ==> dist n ==> dist n) lty2_prod.
   Proof. solve_proper. Qed.
 
-  Instance lty2_sum_ne n : Proper (dist n ==> (dist n ==> dist n)) lty2_sum.
+  Instance lty2_sum_ne n : Proper (dist n ==> dist n ==> dist n) lty2_sum.
   Proof. solve_proper. Qed.
 
   Instance lty2_arr_ne n : Proper (dist n ==> dist n ==> dist n) lty2_arr.
   Proof. solve_proper. Qed.
 
   Instance lty2_rec_ne n : Proper (dist n ==> dist n)
-                                   (lty2_rec : (lty2C Σ -n> lty2C Σ) -> lty2C Σ).
+       (lty2_rec : (lty2C Σ -n> lty2C Σ) -> lty2C Σ).
   Proof.
     intros F F' HF.
     unfold lty2_rec, lty2_car.
@@ -140,28 +147,6 @@ Notation "'ref' A" := (lty2_ref A) : lty_scope.
 Notation "∃ A1 .. An , C" :=
   (lty2_exists (λ A1, .. (lty2_exists (λ An, C%lty2)) ..)) : lty_scope.
 
-Section refinement.
-  Context `{relocG Σ}.
-
-  Definition refines_def (E : coPset)
-           (e e' : expr) (A : lty2 Σ) : iProp Σ :=
-    (∀ ρ, spec_ctx ρ -∗ interp_expr E e e' A)%I.
-  Definition refines_aux : seal refines_def. Proof. by eexists. Qed.
-  Definition refines := unseal refines_aux.
-  Definition refines_eq : refines = refines_def :=
-    seal_eq refines_aux.
-
-  Global Instance refines_ne E n :
-    Proper ((=) ==> (=) ==> (dist n) ==> (dist n)) (refines E).
-  Proof. rewrite refines_eq /refines_def. solve_proper. Qed.
-
-  Global Instance refines_proper E  :
-    Proper ((=) ==> (=) ==> (≡) ==> (≡)) (refines E).
-  Proof. solve_proper_from_ne. Qed.
-End refinement.
-
-Notation "⟦ A ⟧ₑ" := (λ e e', interp_expr ⊤ e e' A).
-
 Section semtypes_properties.
   Context `{relocG Σ}.
 
@@ -199,15 +184,6 @@ Section semtypes_properties.
     compute in Hfoo. eauto.
   Qed.
 
-  Lemma interp_ret (A : lty2 Σ) E e1 e2 v1 v2 :
-    IntoVal e1 v1 →
-    IntoVal e2 v2 →
-    (|={E,⊤}=> A v1 v2)%I -∗ interp_expr E e1 e2 A.
-  Proof.
-    iIntros (<- <-) "HA".
-    iIntros (j K) "Hj /=". iMod "HA".
-    iApply wp_value; eauto.
-  Qed.
 End semtypes_properties.
 
 Notation "'REL' e1 '<<' e2 '@' E ':' A" :=
diff --git a/theories/logic/rules.v b/theories/logic/rules.v
index febbb22f4bfa9168723a8e41122feb5d22249a39..3ab14e39564d17e1673b78de9bf7359ef3a64fc4 100644
--- a/theories/logic/rules.v
+++ b/theories/logic/rules.v
@@ -291,29 +291,6 @@ Section rules.
     by iApply "H".
   Qed.
 
-  Lemma interp_val_arrow (A A' : lty2 Σ) (v v' : val) :
-    (A → A')%lty2 v v' -∗
-    ((∀ (w w' : val), A w w'
-      -∗ REL v w << v' w' : A'))%I.
-  Proof.
-    iIntros "#H". iIntros (v1 v2) "HA".
-    iSpecialize ("H" with "HA").
-    rewrite refines_eq /refines_def.
-    eauto with iFrame.
-  Qed.
-
-  Lemma interp_arrow_val (A A' : lty2 Σ) (v v' : val) ρ :
-    spec_ctx ρ -∗
-    (□ (∀ (w w' : val), A w w'
-         -∗ REL v w << v' w' : A') -∗
-    (A → A')%lty2 v v')%I.
-  Proof.
-    iIntros "#Hs #H". iModIntro. iIntros (v1 v2) "HA".
-    iSpecialize ("H" with "HA").
-    rewrite refines_eq /refines_def.
-    by iApply "H".
-  Qed.
-
   (** * Some derived (symbolic execution) rules *)
 
   (** ** Stateful reductions on the LHS *)
diff --git a/theories/typing/fundamental.v b/theories/typing/fundamental.v
index c6b2641d0988ed901143396dd14ceea341888a8e..15f27ce04ade4826d00b31fbb8b03c51874001e7 100644
--- a/theories/typing/fundamental.v
+++ b/theories/typing/fundamental.v
@@ -22,8 +22,8 @@ Section fundamental.
       fold (bin_log_related E Δ Γ e1 e2 T)
     end.
 
-  Local Ltac intro_clause := progress (iIntros (vs) "#Hvs"; iSimpl).
-  Local Ltac intro_clause' := progress (iIntros (?) "?"; iSimpl).
+  Local Ltac intro_clause := progress (iIntros (vs) "#Hvs /=").
+  Local Ltac intro_clause' := progress (iIntros (?) "? /=").
   Local Ltac value_case := try intro_clause';
     try rel_pure_l; try rel_pure_r; rel_values.
 
@@ -119,9 +119,7 @@ Section fundamental.
     iSpecialize ("Ht" $! vvs' with "[#]").
     { rewrite !binder_insert_fmap.
       iApply (env_ltyped2_insert with "[IH]").
-      - iApply (interp_arrow_val with "Hs").
-        fold interp. (* ?? *)
-        iAlways. iApply "IH".
+      - iApply "IH".
       - iApply (env_ltyped2_insert with "HÏ„1").
         by iFrame. }
 
@@ -154,21 +152,17 @@ Section fundamental.
   Proof.
     iIntros "#H".
     (* TODO: here it is also better to use some sort of characterization
-       of the semantic type for forall *)
+       of the semantic type for forall
+       RK: good idea. *)
     intro_clause.
     iApply refines_spec_ctx. iDestruct 1 as (ρ) "#Hs".
     value_case. rewrite /lty2_forall /lty2_car /=.
     iModIntro. iModIntro. iIntros (A) "!>". iIntros (? ?) "_".
 
-    rewrite /bin_log_related refines_eq /refines_def.
+    rel_pure_l. rel_pure_r.
     iDestruct ("H" $! A) as "#H1".
-    iSpecialize ("H1" with "[Hvs]").
-    { by rewrite (interp_ren A Δ Γ). }
-
-    iIntros (j K) "Hj /=".
-    iModIntro. tp_pure j _. wp_pures. simpl.
-
-    iMod ("H1" with "Hs Hj") as "$".
+    iApply "H1".
+    by rewrite (interp_ren A Δ Γ).
   Qed.
 
   Lemma bin_log_related_tapp' Δ Γ e e' τ τ' :
@@ -181,7 +175,7 @@ Section fundamental.
     intro_clause.
     rel_bind_ap e e' "IH" v v' "IH".
     iSpecialize ("IH" $! (interp τ' Δ)).
-    rewrite interp_val_arrow. iDestruct "IH" as "#IH".
+    iDestruct "IH" as "#IH".
     iSpecialize ("IH" $! #() #() with "[//]").
     by rewrite -interp_subst.
   Qed.
diff --git a/theories/typing/interp.v b/theories/typing/interp.v
index e00cd127cf9f829f0f964c038fc20908c665e9ed..271b1d61474e07f1c65c8ad5d58b1ac379ccf349 100644
--- a/theories/typing/interp.v
+++ b/theories/typing/interp.v
@@ -120,10 +120,10 @@ 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; unfold interp_expr;
+    - intros v1 v2; unfold lty2_car; simpl;
         simpl; properness; auto.
       rewrite /lty2_car /=. properness; auto.
-      apply interp_expr_proper. apply (IHÏ„ (_ :: _)).
+      apply refines_proper=> //. apply (IHÏ„ (_ :: _)).
     - intros ??; unfold lty2_car; simpl; properness; auto. apply (IHÏ„ (_ :: _)).
   Qed.
 
@@ -150,10 +150,10 @@ Section interp_ren.
       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; unfold interp_expr.
+    - intros ??; simpl; unfold lty2_car; simpl;
       properness; auto.
       rewrite /lty2_car /=. properness; auto.
-      apply interp_expr_proper. apply (IHÏ„ (_ :: _)).
+      apply refines_proper=> //. apply (IHÏ„ (_ :: _)).
     - intros ??; unfold lty2_car; simpl; properness; auto.
         by apply (IHÏ„ (_ :: _)).
   Qed.
@@ -178,10 +178,10 @@ Section interp_ren.
         etrans; last by apply HW.
         asimpl. reflexivity. }
       rewrite !lookup_app_r; [|lia ..]. repeat f_equiv. lia.
-    - intros ??. unfold lty2_car; simpl; unfold interp_expr.
+    - intros ??. unfold lty2_car; simpl;
       properness; auto.
       rewrite /lty2_car /=. properness; auto.
-      apply interp_expr_proper. apply (IHÏ„ (_ :: _)).
+      apply refines_proper=>//. apply (IHÏ„ (_ :: _)).
     - intros ??; unfold lty2_car; simpl; properness; auto. apply (IHÏ„ (_ :: _)).
   Qed.