diff --git a/theories/logrel/F_mu_ref_conc/base.v b/theories/logrel/F_mu_ref_conc/base.v
index f544206caf3567d45dd43a04b119df02c66f9e77..8f3f267e173a2a486e11438f68d27cf07c1fa826 100644
--- a/theories/logrel/F_mu_ref_conc/base.v
+++ b/theories/logrel/F_mu_ref_conc/base.v
@@ -18,24 +18,6 @@ Section Autosubst_Lemmas.
   Qed.
 End Autosubst_Lemmas.
 
-Ltac properness :=
-  repeat match goal with
-  | |- (∃ _: _, _)%I ≡ (∃ _: _, _)%I => apply bi.exist_proper =>?
-  | |- (∀ _: _, _)%I ≡ (∀ _: _, _)%I => apply bi.forall_proper =>?
-  | |- (_ ∧ _)%I ≡ (_ ∧ _)%I => apply bi.and_proper
-  | |- (_ ∨ _)%I ≡ (_ ∨ _)%I => apply bi.or_proper
-  | |- (_ → _)%I ≡ (_ → _)%I => apply bi.impl_proper
-  | |- (WP _ {{ _ }})%I ≡ (WP _ {{ _ }})%I => apply wp_proper =>?
-  | |- (▷ _)%I ≡ (▷ _)%I => apply bi.later_proper
-  | |- (□ _)%I ≡ (□ _)%I => apply bi.intuitionistically_proper
-  | |- (_ ∗ _)%I ≡ (_ ∗ _)%I => apply bi.sep_proper
-  | |- (inv _ _)%I ≡ (inv _ _)%I => apply (contractive_proper _)
-  end.
-
-Ltac solve_proper_alt :=
-  repeat intro; (simpl + idtac);
-  by repeat match goal with H : _ ≡{_}≡ _|- _ => rewrite H end.
-
 Reserved Notation "⟦ τ ⟧" (at level 0, τ at level 70).
 Reserved Notation "⟦ τ ⟧ₑ" (at level 0, τ at level 70).
 Reserved Notation "⟦ Γ ⟧*" (at level 0, Γ at level 70).
diff --git a/theories/logrel/F_mu_ref_conc/binary/fundamental.v b/theories/logrel/F_mu_ref_conc/binary/fundamental.v
index 278d64b01d392eed7ad5916159b3d9a6f4a28ab8..83d8c417ee3155426c093959b8f6d68cb8a8d65c 100644
--- a/theories/logrel/F_mu_ref_conc/binary/fundamental.v
+++ b/theories/logrel/F_mu_ref_conc/binary/fundamental.v
@@ -28,13 +28,6 @@ Section fundamental.
   Implicit Types Δ : listO D.
   Local Hint Resolve to_of_val : core.
 
-  Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) ident(w)
-        constr(Hv) uconstr(Hp) :=
-    iApply (wp_bind (fill [ctx]));
-    iApply (wp_wand with "[-]");
-      [iApply Hp; iFrame "#"; trivial|];
-    iIntros (v); iDestruct 1 as (w) Hv; simpl.
-
   (* Put all quantifiers at the outer level *)
   Lemma bin_log_related_alt {Γ e e' τ} Δ vvs j K :
     Γ ⊨ e ≤log≤ e' : τ -∗
@@ -46,6 +39,28 @@ Section fundamental.
     iApply ("Hlog" with "[HΓ]"); iFrame; eauto.
   Qed.
 
+   Lemma interp_expr_bind KK ee Δ τ τ' :
+    ⟦ τ ⟧ₑ Δ ee -∗
+    (∀ vv, ⟦ τ ⟧ Δ vv -∗ ⟦ τ' ⟧ₑ Δ (fill KK.1 (of_val vv.1), fill KK.2 (of_val vv.2))) -∗
+    ⟦ τ' ⟧ₑ Δ (fill KK.1 ee.1, fill KK.2 ee.2).
+  Proof.
+    iIntros "He HK" (j Z) "Hj /=".
+    iSpecialize ("He" with "[Hj]"); first by rewrite -fill_app; iFrame.
+    iApply wp_bind.
+    iApply (wp_wand with "He").
+    iIntros (?); iDestruct 1 as (?) "[? #?]".
+    iApply ("HK" $! (_, _)); [done| rewrite /= fill_app //].
+  Qed.
+
+  Lemma interp_expr_bind' K K' e e' Δ τ τ' :
+    ⟦ τ ⟧ₑ Δ (e, e') -∗
+    (∀ vv, ⟦ τ ⟧ Δ vv -∗ ⟦ τ' ⟧ₑ Δ (fill K (of_val vv.1), fill K' (of_val vv.2))) -∗
+    ⟦ τ' ⟧ₑ Δ (fill K e, fill K' e').
+  Proof. iApply (interp_expr_bind (_, _) (_, _)). Qed.
+
+  Lemma interp_expr_val vv Δ τ : ⟦ τ ⟧ Δ vv -∗ ⟦ τ ⟧ₑ Δ (of_val vv.1, of_val vv.2).
+  Proof. destruct vv; iIntros "?" (? ?) "?"; iApply wp_value; iExists _; iFrame. Qed.
+
   Lemma bin_log_related_var Γ x τ :
     Γ !! x = Some τ → ⊢ Γ ⊨ Var x ≤log≤ Var x : τ.
   Proof.
@@ -79,56 +94,58 @@ Section fundamental.
     Γ ⊨ e2 ≤log≤ e2' : τ2 -∗
     Γ ⊨ Pair e1 e2 ≤log≤ Pair e1' e2' : TProd τ1 τ2.
   Proof.
-    iIntros "#IH1 #IH2" (Δ vvs) "!# #(Hs & HΓ)". iIntros (j K) "Hj /=".
-    smart_wp_bind (PairLCtx e2.[env_subst _]) v v' "[Hv #Hiv]"
-      (bin_log_related_alt _ _ j ((PairLCtx e2'.[env_subst _]) :: K) with "IH1").
-    smart_wp_bind (PairRCtx v) w w' "[Hw #Hiw]"
-      (bin_log_related_alt _ _ j ((PairRCtx v') :: K) with "IH2").
-    iApply wp_value. iExists (PairV v' w'); iFrame "Hw".
+    iIntros "#IH1 #IH2" (Δ vvs) "!# #(Hs & HΓ)".
+    iApply (interp_expr_bind' [PairLCtx _] [PairLCtx _]); first by iApply "IH1"; iFrame "#".
+    iIntros ([v v']) "Hvv".
+    iApply (interp_expr_bind' [PairRCtx _] [PairRCtx _]); first by iApply "IH2"; iFrame "#".
+    iIntros ([w w']) "Hww".
+    iApply (interp_expr_val (PairV _ _, PairV _ _)).
     iExists (v, v'), (w, w'); simpl; repeat iSplit; trivial.
   Qed.
 
   Lemma bin_log_related_fst Γ e e' τ1 τ2 :
     Γ ⊨ e ≤log≤ e' : TProd τ1 τ2 -∗ Γ ⊨ Fst e ≤log≤ Fst e' : τ1.
   Proof.
-    iIntros "#IH" (Δ vvs) "!# #(Hs & HΓ)"; iIntros (j K) "Hj /=".
-    smart_wp_bind (FstCtx) v v' "[Hv #Hiv]"
-      (bin_log_related_alt _ _ j (FstCtx :: K) with "[IH]"); cbn.
-    iDestruct "Hiv" as ([w1 w1'] [w2 w2']) "#[% [Hw1 Hw2]]"; simplify_eq.
+    iIntros "#IH" (Δ vvs) "!# #(Hs & HΓ)".
+    iApply (interp_expr_bind' [FstCtx] [FstCtx]); first by iApply "IH"; iFrame "#".
+    iIntros ([v v']) "Hvv"; cbn [interp].
+    iDestruct "Hvv" as ([w1 w1'] [w2 w2']) "#[% [Hw1 Hw2]]"; simplify_eq/=.
+    iIntros (j K) "Hj /=".
     iApply wp_pure_step_later; eauto. iIntros "!> _".
-    iMod (step_fst with "[Hs Hv]") as "Hw"; eauto.
+    iMod (step_fst with "[$]") as "Hw"; eauto.
     iApply wp_value; eauto.
   Qed.
 
   Lemma bin_log_related_snd Γ e e' τ1 τ2 :
     Γ ⊨ e ≤log≤ e' : TProd τ1 τ2 -∗ Γ ⊨ Snd e ≤log≤ Snd e' : τ2.
   Proof.
-    iIntros "#IH" (Δ vvs) "!# #(Hs & HΓ)"; iIntros (j K) "Hj /=".
-    smart_wp_bind (SndCtx) v v' "[Hv #Hiv]"
-      (bin_log_related_alt _ _ j (SndCtx :: K) with "IH"); cbn.
-    iDestruct "Hiv" as ([w1 w1'] [w2 w2']) "#[% [Hw1 Hw2]]"; simplify_eq.
+    iIntros "#IH" (Δ vvs) "!# #(Hs & HΓ)".
+    iApply (interp_expr_bind' [SndCtx] [SndCtx]); first by iApply "IH"; iFrame "#".
+    iIntros ([v v']) "Hvv"; cbn [interp].
+    iDestruct "Hvv" as ([w1 w1'] [w2 w2']) "#[% [Hw1 Hw2]]"; simplify_eq.
+    iIntros (j K) "Hj /=".
     iApply wp_pure_step_later; eauto. iIntros "!> _".
-    iMod (step_snd with "[Hs Hv]") as "Hw"; eauto.
+    iMod (step_snd with "[$]") as "Hw"; eauto.
     iApply wp_value; eauto.
   Qed.
 
   Lemma bin_log_related_injl Γ e e' τ1 τ2 :
     Γ ⊨ e ≤log≤ e' : τ1 -∗ Γ ⊨ InjL e ≤log≤ InjL e' : (TSum τ1 τ2).
   Proof.
-    iIntros "#IH" (Δ vvs) "!# #(Hs & HΓ)"; iIntros (j K) "Hj /=".
-    smart_wp_bind (InjLCtx) v v' "[Hv #Hiv]"
-      (bin_log_related_alt _ _ j (InjLCtx :: K) with "IH"); cbn.
-    iApply wp_value. iExists (InjLV v'); iFrame "Hv".
+    iIntros "#IH" (Δ vvs) "!# #(Hs & HΓ)".
+    iApply (interp_expr_bind' [InjLCtx] [InjLCtx]); first by iApply "IH"; iFrame "#".
+    iIntros ([v v']) "Hvv".
+    iApply (interp_expr_val (InjLV _, InjLV _)).
     iLeft; iExists (_,_); eauto 10.
   Qed.
 
   Lemma bin_log_related_injr Γ e e' τ1 τ2 :
       Γ ⊨ e ≤log≤ e' : τ2 -∗ Γ ⊨ InjR e ≤log≤ InjR e' : TSum τ1 τ2.
   Proof.
-    iIntros "#IH" (Δ vvs) "!# #(Hs & HΓ)"; iIntros (j K) "Hj /=".
-    smart_wp_bind (InjRCtx) v v' "[Hv #Hiv]"
-      (bin_log_related_alt _ _ j (InjRCtx :: K) with "IH"); cbn.
-    iApply wp_value. iExists (InjRV v'); iFrame "Hv".
+    iIntros "#IH" (Δ vvs) "!# #(Hs & HΓ)".
+    iApply (interp_expr_bind' [InjRCtx] [InjRCtx]); first by iApply "IH"; iFrame "#".
+    iIntros ([v v']) "Hvv".
+    iApply (interp_expr_val (InjRV _, InjRV _)).
     iRight; iExists (_,_); eauto 10.
   Qed.
 
@@ -138,21 +155,22 @@ Section fundamental.
     τ2 :: Γ ⊨ e2 ≤log≤ e2' : τ3 -∗
     Γ ⊨ Case e0 e1 e2 ≤log≤ Case e0' e1' e2' : τ3.
   Proof.
-    iIntros "#IH1 #IH2 #IH3" (Δ vvs) "!# #(Hs & HΓ)"; iIntros (j K) "Hj /=".
+    iIntros "#IH1 #IH2 #IH3" (Δ vvs) "!# #(Hs & HΓ)".
     iDestruct (interp_env_length with "HΓ") as %?.
-    smart_wp_bind (CaseCtx _ _) v v' "[Hv #Hiv]"
-      (bin_log_related_alt _ _ j ((CaseCtx _ _) :: K) with "IH1"); cbn.
-    iDestruct "Hiv" as "[Hiv|Hiv]";
-    iDestruct "Hiv" as ([w w']) "[% Hw]"; simplify_eq.
+    iApply (interp_expr_bind' [CaseCtx _ _] [CaseCtx _ _]); first by iApply "IH1"; iFrame "#".
+    iIntros ([v v']) "Hvv /=".
+    iIntros (j K) "Hj /=".
+    iDestruct "Hvv" as "[Hvv|Hvv]";
+    iDestruct "Hvv" as ([w w']) "[% Hw]"; simplify_eq.
     - iApply fupd_wp.
-      iMod (step_case_inl with "[Hs Hv]") as "Hz"; eauto.
+      iMod (step_case_inl with "[$]") as "Hz"; eauto.
       iApply wp_pure_step_later; auto. fold of_val. iIntros "!> !> _".
       asimpl.
       iApply (bin_log_related_alt _ ((w,w') :: vvs) with "IH2").
       repeat iSplit; eauto.
       iApply interp_env_cons; auto.
     - iApply fupd_wp.
-      iMod (step_case_inr with "[Hs Hv]") as "Hz"; eauto.
+      iMod (step_case_inr with "[$]") as "Hz"; eauto.
       iApply wp_pure_step_later; auto. fold of_val. iIntros "!> !> _".
       asimpl.
       iApply (bin_log_related_alt _ ((w,w') :: vvs) with "IH3").
@@ -166,10 +184,11 @@ Section fundamental.
     Γ ⊨ e2 ≤log≤ e2' : τ -∗
     Γ ⊨ If e0 e1 e2 ≤log≤ If e0' e1' e2' : τ.
   Proof.
-    iIntros "#IH1 #IH2 #IH3" (Δ vvs) "!# #(Hs & HΓ)"; iIntros (j K) "Hj /=".
-    smart_wp_bind (IfCtx _ _) v v' "[Hv #Hiv]"
-      (bin_log_related_alt _ _ j ((IfCtx _ _) :: K) with "IH1"); cbn.
-    iDestruct "Hiv" as ([]) "[% %]"; simplify_eq/=; iApply fupd_wp.
+    iIntros "#IH1 #IH2 #IH3" (Δ vvs) "!# #(Hs & HΓ)".
+    iApply (interp_expr_bind' [IfCtx _ _] [IfCtx _ _]); first by iApply "IH1"; iFrame "#".
+    iIntros ([v v']) "Hvv /=".
+    iIntros (j K) "Hj /=".
+    iDestruct "Hvv" as ([]) "[% %]"; simplify_eq/=; iApply fupd_wp.
     - iMod (step_if_true _ j K with "[-]") as "Hz"; eauto.
       iApply wp_pure_step_later; auto. iIntros "!> !> _".
       iApply (bin_log_related_alt with "IH2"); eauto.
@@ -183,13 +202,14 @@ Section fundamental.
     Γ ⊨ e2 ≤log≤ e2' : TNat -∗
     Γ ⊨ BinOp op e1 e2 ≤log≤ BinOp op e1' e2' : binop_res_type op.
   Proof.
-    iIntros "#IH1 #IH2" (Δ vvs) "!# #(Hs & HΓ)"; iIntros (j K) "Hj /=".
-    smart_wp_bind (BinOpLCtx _ _) v v' "[Hv #Hiv]"
-                  (bin_log_related_alt _ _ j ((BinOpLCtx _ _) :: K) with "IH1"); cbn.
-    smart_wp_bind (BinOpRCtx _ _) w w' "[Hw #Hiw]"
-                  (bin_log_related_alt _ _ j ((BinOpRCtx _ _) :: K) with "IH2"); cbn.
-    iDestruct "Hiv" as (n) "[% %]"; simplify_eq/=.
-    iDestruct "Hiw" as (n') "[% %]"; simplify_eq/=.
+    iIntros "#IH1 #IH2" (Δ vvs) "!# #(Hs & HΓ)".
+    iApply (interp_expr_bind' [BinOpLCtx _ _] [BinOpLCtx _ _]); first by iApply "IH1"; iFrame "#".
+    iIntros ([v v']) "Hvv /=".
+    iApply (interp_expr_bind' [BinOpRCtx _ _] [BinOpRCtx _ _]); first by iApply "IH2"; iFrame "#".
+    iIntros ([w w']) "Hww /=".
+    iIntros (j K) "Hj /=".
+    iDestruct "Hvv" as (n) "[% %]"; simplify_eq/=.
+    iDestruct "Hww" as (n') "[% %]"; simplify_eq/=.
     iApply fupd_wp.
     iMod (step_nat_binop _ j K with "[-]") as "Hz"; eauto.
     iApply wp_pure_step_later; auto. iIntros "!> !> _".
@@ -202,9 +222,10 @@ Section fundamental.
     TArrow τ1 τ2 :: τ1 :: Γ ⊨ e ≤log≤ e' : τ2 -∗
     Γ ⊨ Rec e ≤log≤ Rec e' : TArrow τ1 τ2.
   Proof.
-    iIntros "#IH" (Δ vvs) "!# #(Hs & HΓ)"; iIntros (j K) "Hj /=".
-    iApply wp_value. iExists (RecV _). iIntros "{$Hj} !#".
-    iLöb as "IHL". iIntros ([v v']) "#Hiv". iIntros (j' K') "Hj".
+    iIntros "#IH" (Δ vvs) "!# #(Hs & HΓ)".
+    iApply (interp_expr_val (RecV _, RecV _)).
+    simpl.
+    iLöb as "IHL". iIntros ([v v']) "!# #Hiv". iIntros (j' K') "Hj".
     iDestruct (interp_env_length with "HΓ") as %?.
     iApply wp_pure_step_later; auto 1 using to_of_val. iIntros "!> _".
     iApply fupd_wp.
@@ -220,9 +241,10 @@ Section fundamental.
     τ1 :: Γ ⊨ e ≤log≤ e' : τ2 -∗
     Γ ⊨ Lam e ≤log≤ Lam e' : TArrow τ1 τ2.
   Proof.
-    iIntros "#IH" (Δ vvs) "!# #(Hs & HΓ)"; iIntros (j K) "Hj /=".
-    iApply wp_value. iExists (LamV _). iIntros "{$Hj} !#".
-    iIntros ([v v']) "#Hiv". iIntros (j' K') "Hj".
+    iIntros "#IH" (Δ vvs) "!# #(Hs & HΓ)".
+    iApply (interp_expr_val (LamV _, LamV _)).
+    simpl.
+    iIntros ([v v']) "!# #Hiv". iIntros (j' K') "Hj".
     iDestruct (interp_env_length with "HΓ") as %?.
     iApply wp_pure_step_later; auto 1 using to_of_val. iIntros "!> _".
     iApply fupd_wp.
@@ -239,10 +261,11 @@ Section fundamental.
     τ1 :: Γ ⊨ e2 ≤log≤ e2' : τ2 -∗
     Γ ⊨ LetIn e1 e2 ≤log≤ LetIn e1' e2': τ2.
   Proof.
-    iIntros "#IH1 #IH2" (Δ vvs) "!# #(Hs & HΓ)"; iIntros (j K) "Hj /=".
+    iIntros "#IH1 #IH2" (Δ vvs) "!# #(Hs & HΓ)".
     iDestruct (interp_env_length with "HΓ") as %?.
-    smart_wp_bind (LetInCtx _) v v' "[Hv #Hiv]"
-      (bin_log_related_alt _ _ j ((LetInCtx _) :: K) with "IH1"); cbn.
+    iApply (interp_expr_bind' [LetInCtx _] [LetInCtx _]); first by iApply "IH1"; iFrame "#".
+    iIntros ([v v']) "#Hvv /=".
+    iIntros (j K) "Hj /=".
     iMod (step_letin _ j K with "[-]") as "Hz"; eauto.
     iApply wp_pure_step_later; auto. iIntros "!> _".
     asimpl.
@@ -256,10 +279,11 @@ Section fundamental.
     Γ ⊨ e2 ≤log≤ e2' : τ2 -∗
     Γ ⊨ Seq e1 e2 ≤log≤ Seq e1' e2': τ2.
   Proof.
-    iIntros "#IH1 #IH2" (Δ vvs) "!# #(Hs & HΓ)"; iIntros (j K) "Hj /=".
+    iIntros "#IH1 #IH2" (Δ vvs) "!# #(Hs & HΓ)".
     iDestruct (interp_env_length with "HΓ") as %?.
-    smart_wp_bind (SeqCtx _) v v' "[Hv #Hiv]"
-      (bin_log_related_alt _ _ j ((SeqCtx _) :: K) with "IH1"); cbn.
+    iApply (interp_expr_bind' [SeqCtx _] [SeqCtx _]); first by iApply "IH1"; iFrame "#".
+    iIntros ([v v']) "#Hvv /=".
+    iIntros (j K) "Hj /=".
     iMod (step_seq _ j K with "[-]") as "Hz"; eauto.
     iApply wp_pure_step_later; auto. iIntros "!> _".
     asimpl.
@@ -271,13 +295,13 @@ Section fundamental.
     Γ ⊨ e2 ≤log≤ e2' : τ1 -∗
     Γ ⊨ App e1 e2 ≤log≤ App e1' e2' :  τ2.
   Proof.
-    iIntros "#IH1 #IH2" (Δ vvs) "!# #(Hs & HΓ)"; iIntros (j K) "Hj /=".
-    smart_wp_bind (AppLCtx (e2.[env_subst (vvs.*1)])) v v' "[Hv #Hiv]"
-      (bin_log_related_alt
-        _ _ j (((AppLCtx (e2'.[env_subst (vvs.*2)]))) :: K) with "IH1"); cbn.
-    smart_wp_bind (AppRCtx v) w w' "[Hw #Hiw]"
-      (bin_log_related_alt _ _ j ((AppRCtx v') :: K) with "IH2"); cbn.
-    iApply ("Hiv" $! (w, w') with "Hiw"); simpl; eauto.
+    iIntros "#IH1 #IH2" (Δ vvs) "!# #(Hs & HΓ) /=".
+    iApply (interp_expr_bind' [AppLCtx _] [AppLCtx _]); first by iApply "IH1"; iFrame "#".
+    simpl.
+    iIntros ([v v']) "#Hvv /=".
+    iApply (interp_expr_bind' [AppRCtx _] [AppRCtx _]); first by iApply "IH2"; iFrame "#".
+    iIntros ([w w']) "#Hww/=".
+    iApply ("Hvv" $! (w, w') with "Hww"); simpl; eauto.
   Qed.
 
   Lemma bin_log_related_tlam Γ e e' τ :
@@ -298,12 +322,13 @@ Section fundamental.
   Lemma bin_log_related_tapp Γ e e' τ τ' :
     Γ ⊨ e ≤log≤ e' : TForall τ -∗ Γ ⊨ TApp e ≤log≤ TApp e' : τ.[τ'/].
   Proof.
-    iIntros "#IH" (Δ vvs) "!# #(Hs & HΓ)"; iIntros (j K) "Hj /=".
-    smart_wp_bind (TAppCtx) v v' "[Hj #Hv]"
-      (bin_log_related_alt _ _ j (TAppCtx :: K) with "IH"); cbn.
-    rewrite -/interp.
+    iIntros "#IH" (Δ vvs) "!# #(Hs & HΓ)".
+    iApply (interp_expr_bind' [TAppCtx] [TAppCtx]); first by iApply "IH"; iFrame "#".
+    simpl.
+    iIntros ([v v']) "#Hvv /=".
+    iIntros (j K) "Hj /=".
     iApply wp_wand_r; iSplitL.
-    { iSpecialize ("Hv" $! (interp τ' Δ)). iApply "Hv"; eauto. }
+    { iSpecialize ("Hvv" $! (interp τ' Δ)). iApply "Hvv"; eauto. }
     iIntros (w). iDestruct 1 as (w') "[Hw Hiw]".
     iExists _; rewrite -interp_subst; eauto.
   Qed.
@@ -311,13 +336,11 @@ Section fundamental.
   Lemma bin_log_related_pack Γ e e' τ τ' :
     Γ ⊨ e ≤log≤ e' : τ.[τ'/] -∗ Γ ⊨ Pack e ≤log≤ Pack e' : TExist τ.
   Proof.
-    iIntros "#IH" (Δ vvs) "!# #(Hs & HΓ)"; iIntros (j K) "Hj /=".
-    smart_wp_bind (PackCtx) v v' "[Hj #Hv]"
-      (bin_log_related_alt _ _ j (PackCtx :: K) with "IH"); cbn.
-    iApply wp_value.
-    iExists (PackV _); iFrame.
-    iModIntro.
-    rewrite -interp_subst.
+    iIntros "#IH" (Δ vvs) "!# #(Hs & HΓ)".
+    iApply (interp_expr_bind' [PackCtx] [PackCtx]); first by iApply "IH"; iFrame "#".
+    iIntros ([v v']) "#Hvv".
+    iApply (interp_expr_val (PackV _, PackV _)).
+    rewrite -interp_subst /=.
     iExists (interp _ Δ), (_, _); iSplit; done.
   Qed.
 
@@ -326,11 +349,11 @@ Section fundamental.
     τ :: (subst (ren (+1)) <$> Γ) ⊨ e2 ≤log≤ e2' : τ'.[ren (+1)] -∗
     Γ ⊨ UnpackIn e1 e2 ≤log≤ UnpackIn e1' e2' : τ'.
   Proof.
-    iIntros "#IH1 #IH2" (Δ vvs) "!# #(Hs & HΓ)"; iIntros (j K) "Hj /=".
-    smart_wp_bind (UnpackInCtx _) v v' "[Hj #Hv]"
-      (bin_log_related_alt _ _ j (UnpackInCtx _ :: K) with "IH1"); cbn.
-    rewrite -/interp.
-    iDestruct "Hv" as (τi (v1, v2) Hvv) "#Hvv"; simplify_eq /=.
+    iIntros "#IH1 #IH2" (Δ vvs) "!# #(Hs & HΓ)".
+    iApply (interp_expr_bind' [UnpackInCtx _] [UnpackInCtx _]); first by iApply "IH1"; iFrame "#".
+    iIntros ([v v']) "#Hvv /=".
+    iDestruct "Hvv" as (τi (v1, v2) Hvv) "#Hvv"; simplify_eq /=.
+    iIntros (j K) "Hj /=".
     iApply wp_pure_step_later; auto. iIntros "!> _".
     iApply fupd_wp.
     iMod (step_pack with "[Hj]") as "Hj"; eauto.
@@ -349,27 +372,24 @@ Section fundamental.
   Lemma bin_log_related_fold Γ e e' τ :
     Γ ⊨ e ≤log≤ e' : τ.[(TRec τ)/] -∗ Γ ⊨ Fold e ≤log≤ Fold e' : TRec τ.
   Proof.
-    iIntros "#IH" (Δ vvs) "!# #(Hs & HΓ)"; iIntros (j K) "Hj /=".
-    iApply (wp_bind (fill [FoldCtx])); iApply wp_wand_l; iSplitR;
-        [|iApply (bin_log_related_alt _ _ j (FoldCtx :: K) with "IH");
-          simpl; repeat iSplitR; trivial].
-    iIntros (v); iDestruct 1 as (w) "[Hv #Hiv]".
-    iApply wp_value. iExists (FoldV w); iFrame "Hv".
-    rewrite fixpoint_interp_rec1_eq /= -interp_subst.
+    iIntros "#IH" (Δ vvs) "!# #(Hs & HΓ)".
+    iApply (interp_expr_bind' [FoldCtx] [FoldCtx]); first by iApply "IH"; iFrame "#".
+    iIntros ([v v']) "#Hvv".
+    iApply (interp_expr_val (FoldV _, FoldV _)).
+    rewrite /= fixpoint_interp_rec1_eq /= -interp_subst.
     iModIntro; iExists (_, _); eauto.
   Qed.
 
   Lemma bin_log_related_unfold Γ e e' τ :
     Γ ⊨ e ≤log≤ e' : TRec τ -∗ Γ ⊨ Unfold e ≤log≤ Unfold e' : τ.[(TRec τ)/].
   Proof.
-    iIntros "#IH" (Δ vvs) "!# #(Hs & HΓ)"; iIntros (j K) "Hj /=".
-    iApply (wp_bind (fill [UnfoldCtx])); iApply wp_wand_l; iSplitR;
-        [|iApply (bin_log_related_alt _ _ j (UnfoldCtx :: K) with "IH");
-          simpl; repeat iSplitR; trivial].
-    iIntros (v). iDestruct 1 as (v') "[Hw #Hiw]".
+    iIntros "#IH" (Δ vvs) "!# #(Hs & HΓ)".
+    iApply (interp_expr_bind' [UnfoldCtx] [UnfoldCtx]); first by iApply "IH"; iFrame "#".
+    iIntros ([v v']) "#Hvv".
+    iIntros (j K) "Hj /=".
     rewrite /= fixpoint_interp_rec1_eq /=.
     change (fixpoint _) with (interp (TRec τ) Δ).
-    iDestruct "Hiw" as ([w w']) "#[% Hiz]"; simplify_eq/=.
+    iDestruct "Hvv" as ([w w']) "#[% Hiz]"; simplify_eq/=.
     iApply fupd_wp.
     iMod (step_fold _ j K (of_val w') w' with "[-]") as "Hz"; eauto.
     iApply wp_pure_step_later; auto. iIntros "!> !> _".
@@ -390,9 +410,10 @@ Section fundamental.
   Lemma bin_log_related_alloc Γ e e' τ :
       Γ ⊨ e ≤log≤ e' : τ -∗ Γ ⊨ Alloc e ≤log≤ Alloc e' : Tref τ.
   Proof.
-    iIntros "#IH" (Δ vvs) "!# #(Hs & HΓ)"; iIntros (j K) "Hj /=".
-    smart_wp_bind (AllocCtx) v v' "[Hv #Hiv]"
-      (bin_log_related_alt _ _ j (AllocCtx :: K) with "IH").
+    iIntros "#IH" (Δ vvs) "!# #(Hs & HΓ)".
+    iApply (interp_expr_bind' [AllocCtx] [AllocCtx]); first by iApply "IH"; iFrame "#".
+    iIntros ([v v']) "#Hvv".
+    iIntros (j K) "Hj /=".
     iApply fupd_wp.
     iMod (step_alloc _ j K (of_val v') v' with "[-]") as (l') "[Hj Hl]"; eauto.
     iApply wp_atomic; eauto.
@@ -400,25 +421,24 @@ Section fundamental.
     iIntros (l) "Hl'".
     iMod (inv_alloc (logN .@ (l,l')) _ (∃ w : val * val,
       l ↦ᵢ w.1 ∗ l' ↦ₛ w.2 ∗ interp τ Δ w)%I with "[Hl Hl']") as "HN"; eauto.
-    { iNext. iExists (v, v'); iFrame. iFrame "Hiv". }
+    { iNext. iExists (v, v'); iFrame; done. }
     iModIntro; iExists (LocV l'). iFrame "Hj". iExists (l, l'); eauto.
   Qed.
 
   Lemma bin_log_related_load Γ e e' τ :
     Γ ⊨ e ≤log≤ e' : (Tref τ) -∗ Γ ⊨ Load e ≤log≤ Load e' : τ.
   Proof.
-    iIntros "#IH" (Δ vvs) "!# #(Hs & HΓ)"; iIntros (j K) "Hj /=".
-    smart_wp_bind (LoadCtx) v v' "[Hv #Hiv]"
-      (bin_log_related_alt _ _ j (LoadCtx :: K) with "IH").
-    iDestruct "Hiv" as ([l l']) "[% Hinv]"; simplify_eq/=.
+    iIntros "#IH" (Δ vvs) "!# #(Hs & HΓ)".
+    iApply (interp_expr_bind' [LoadCtx] [LoadCtx]); first by iApply "IH"; iFrame "#".
+    iIntros ([v v']) "#Hvv".
+    iIntros (j K) "Hj /=".
+    iDestruct "Hvv" as ([l l']) "[% Hinv]"; simplify_eq/=.
     iApply wp_atomic; eauto.
     iInv (logN .@ (l,l')) as ([w w']) "[Hw1 [>Hw2 #Hw]]" "Hclose"; simpl.
-    (* TODO: why can we eliminate the next modality here? ↑ *)
     iModIntro.
     iApply (wp_load with "Hw1").
     iNext. iIntros "Hw1".
-    iMod (step_load  with "[Hv Hw2]") as "[Hv Hw2]";
-      [solve_ndisj|by iFrame|].
+    iMod (step_load  with "[$]") as "[Hv Hw2]"; first solve_ndisj.
     iMod ("Hclose" with "[Hw1 Hw2]").
     { iNext. iExists (w,w'); by iFrame. }
     iModIntro. iExists w'; by iFrame.
@@ -429,21 +449,21 @@ Section fundamental.
     Γ ⊨ e2 ≤log≤ e2' : τ -∗
     Γ ⊨ Store e1 e2 ≤log≤ Store e1' e2' : TUnit.
   Proof.
-    iIntros "#IH1 #IH2" (Δ vvs) "!# #(Hs & HΓ)"; iIntros (j K) "Hj /=".
-    smart_wp_bind (StoreLCtx _) v v' "[Hv #Hiv]"
-      (bin_log_related_alt _ _ j ((StoreLCtx _) :: K) with "IH1").
-    smart_wp_bind (StoreRCtx _) w w' "[Hw #Hiw]"
-      (bin_log_related_alt _ _ j ((StoreRCtx _) :: K) with "IH2").
-    iDestruct "Hiv" as ([l l']) "[% Hinv]"; simplify_eq/=.
+    iIntros "#IH1 #IH2" (Δ vvs) "!# #(Hs & HΓ)".
+    iApply (interp_expr_bind' [StoreLCtx _] [StoreLCtx _]); first by iApply "IH1"; iFrame "#".
+    iIntros ([v v']) "#Hvv".
+    iApply (interp_expr_bind' [StoreRCtx _] [StoreRCtx _]); first by iApply "IH2"; iFrame "#".
+    iIntros ([w w']) "#Hww".
+    iIntros (j K) "Hj /=".
+    iDestruct "Hvv" as ([l l']) "[% Hinv]"; simplify_eq/=.
     iApply wp_atomic; eauto.
     iInv (logN .@ (l,l')) as ([v v']) "[Hv1 [>Hv2 #Hv]]" "Hclose".
     iModIntro.
     iApply (wp_store with "Hv1"); auto using to_of_val.
     iNext. iIntros "Hw2".
-    iMod (step_store with "[$Hs Hw Hv2]") as "[Hw Hv2]"; eauto;
-    [solve_ndisj | by iFrame|].
+    iMod (step_store with "[$]") as "[Hw Hv2]"; [done|solve_ndisj|].
     iMod ("Hclose" with "[Hw2 Hv2]").
-    { iNext; iExists (w, w'); simpl; iFrame. iFrame "Hiw". }
+    { iNext; iExists (w, w'); simpl; iFrame; done. }
     iExists UnitV; iFrame; auto.
   Qed.
 
@@ -455,40 +475,33 @@ Section fundamental.
     Γ ⊨ CAS e1 e2 e3 ≤log≤ CAS e1' e2' e3' : TBool.
   Proof.
     iIntros (Heqτ) "#IH1 #IH2 #IH3".
-    iIntros (Δ vvs) "!# #(Hs & HΓ)"; iIntros (j K) "Hj /=".
-    smart_wp_bind (CasLCtx _ _) v v' "[Hv #Hiv]"
-      (bin_log_related_alt _ _ j ((CasLCtx _ _) :: K) with "IH1").
-    smart_wp_bind (CasMCtx _ _) w w' "[Hw #Hiw]"
-      (bin_log_related_alt _ _ j ((CasMCtx _ _) :: K) with "IH2").
-    smart_wp_bind (CasRCtx _ _) u u' "[Hu #Hiu]"
-      (bin_log_related_alt _ _ j ((CasRCtx _ _) :: K) with "IH3").
-    iDestruct "Hiv" as ([l l']) "[% Hinv]"; simplify_eq/=.
+    iIntros (Δ vvs) "!# #(Hs & HΓ)".
+    iApply (interp_expr_bind' [CasLCtx _ _] [CasLCtx _ _]); first by iApply "IH1"; iFrame "#".
+    iIntros ([v v']) "#Hvv".
+    iApply (interp_expr_bind' [CasMCtx _ _] [CasMCtx _ _]); first by iApply "IH2"; iFrame "#".
+    iIntros ([w w']) "#Hww".
+    iApply (interp_expr_bind' [CasRCtx _ _] [CasRCtx _ _]); first by iApply "IH3"; iFrame "#".
+    iIntros ([u u']) "#Huu".
+    iIntros (j K) "Hj /=".
+    iDestruct "Hvv" as ([l l']) "[% Hinv]"; simplify_eq/=.
     iApply wp_atomic; eauto.
-    iMod (interp_ref_open' _ _ l l' with "[]") as
-        (v v') "(>Hl & >Hl' & #Hiv & Heq & Hcl)"; eauto.
-    { iExists (_, _); eauto. }
+    iInv (logN.@(l, l')) as ([v v']) "(>Hl & >Hl' & #Hvv) /=" "Hclose".
     iModIntro.
-    destruct (decide (v = w)) as [|Hneq]; subst.
+    destruct (decide (v = w)) as [|Hneq]; simplify_eq.
     - iApply (wp_cas_suc with "Hl"); eauto using to_of_val; eauto.
       iNext. iIntros "Hl".
-      iMod ("Heq" with "Hl Hl' Hiv Hiw") as "(Hl & Hl' & Heq)".
-      iDestruct "Heq" as %[-> _]; last trivial.
-      iMod (step_cas_suc
-            with "[Hu Hl']") as "[Hw Hl']"; simpl; eauto; first solve_ndisj.
-      { iFrame. iFrame "Hs". }
-      iMod ("Hcl" with "[Hl Hl']").
+      iMod (interp_EqType_one_to_one with "Hl Hl' Hvv Hww") as "(Hl & Hl' & %)"; first done.
+      destruct (decide (v' = w')); simplify_eq; last by intuition simplify_eq.
+      iMod (step_cas_suc with "[$]") as "[Hw Hl']"; simpl; eauto; first solve_ndisj.
+      iMod ("Hclose" with "[Hl Hl']").
       { iNext; iExists (_, _); by iFrame. }
       iExists (#♭v true); iFrame; eauto.
     - iApply (wp_cas_fail with "Hl"); eauto using to_of_val; eauto.
       iNext. iIntros "Hl".
-      iMod ("Heq" with "Hl Hl' Hiv Hiw") as "(Hl & Hl' & Heq)".
-      iDestruct "Heq" as %[_ Heq].
-      assert (v' ≠ w').
-      { by intros ?; apply Hneq; rewrite Heq. }
-      iMod (step_cas_fail
-            with "[$Hs Hu Hl']") as "[Hw Hl']"; simpl; eauto; first solve_ndisj.
-      { iFrame. }
-      iMod ("Hcl" with "[Hl Hl']").
+      iMod (interp_EqType_one_to_one with "Hl Hl' Hvv Hww") as "(Hl & Hl' & %)"; first done.
+      destruct (decide (v' = w')); simplify_eq; first by intuition simplify_eq.
+      iMod (step_cas_fail with "[$]") as "[Hw Hl']"; simpl; eauto; first solve_ndisj.
+      iMod ("Hclose" with "[Hl Hl']").
       { iNext; iExists (_, _); by iFrame. }
       iExists (#♭v false); eauto.
   Qed.
@@ -498,21 +511,21 @@ Section fundamental.
     Γ ⊨ e2 ≤log≤ e2' : TNat -∗
     Γ ⊨ FAA e1 e2 ≤log≤ FAA e1' e2' : TNat.
   Proof.
-    iIntros "#IH1 #IH2" (Δ vvs) "!# #(Hs & HΓ)"; iIntros (j K) "Hj /=".
-    smart_wp_bind (FAALCtx _) v v' "[Hv #Hiv]"
-      (bin_log_related_alt _ _ j ((FAALCtx _) :: K) with "IH1").
-    iDestruct "Hiv" as ([l l'] ?) "Hll"; simplify_eq.
-    smart_wp_bind (FAARCtx _) u u' "[Hu #Hiu]"
-      (bin_log_related_alt _ _ j ((FAARCtx _) :: K) with "IH2").
-    iDestruct "Hiu" as (m) "[% %]"; simplify_eq.
+    iIntros "#IH1 #IH2" (Δ vvs) "!# #(Hs & HΓ)".
+    iApply (interp_expr_bind' [FAALCtx _] [FAALCtx _]); first by iApply "IH1"; iFrame "#".
+    iIntros ([v v']) "#Hvv".
+    iApply (interp_expr_bind' [FAARCtx _] [FAARCtx _]); first by iApply "IH2"; iFrame "#".
+    iIntros ([w w']) "#Hww".
+    iIntros (j K) "Hj /=".
+    iDestruct "Hvv" as ([l l']) "[% Hinv]"; simplify_eq/=.
+    iDestruct "Hww" as (m) "[% %]"; simplify_eq.
     iApply wp_atomic; eauto.
     iInv (logN .@ (l,l')) as ([v v']) "[Hv1 [>Hv2 #>Hv]]" "Hclose".
     iDestruct "Hv" as (?) "[% %]"; simplify_eq/=.
     iModIntro.
     iApply (wp_FAA with "Hv1"); auto using to_of_val.
     iNext. iIntros "Hw2".
-    iMod (step_faa with "[$Hu Hv2]") as "[Hu Hv2]"; eauto;
-      first solve_ndisj.
+    iMod (step_faa with "[$]") as "[Hu Hv2]"; eauto; first solve_ndisj.
     iMod ("Hclose" with "[Hw2 Hv2]").
     { iNext; iExists (#nv _, #nv _); simpl; iFrame. by eauto. }
     iModIntro.
diff --git a/theories/logrel/F_mu_ref_conc/binary/logrel.v b/theories/logrel/F_mu_ref_conc/binary/logrel.v
index d7266cd5687a23c2b3705d1b2f1377a74b44c089..83746b9dc6ca37d92ae2c667465844e10f6ec70d 100644
--- a/theories/logrel/F_mu_ref_conc/binary/logrel.v
+++ b/theories/logrel/F_mu_ref_conc/binary/logrel.v
@@ -9,23 +9,6 @@ From iris_examples.logrel.F_mu_ref_conc Require Export typing.
 From iris.prelude Require Import options.
 Import uPred.
 
-(* HACK: move somewhere else *)
-Ltac auto_equiv :=
-  (* Deal with "pointwise_relation" *)
-  repeat lazymatch goal with
-  | |- pointwise_relation _ _ _ _ => intros ?
-  end;
-  (* Normalize away equalities. *)
-  repeat match goal with
-  | H : _ ≡{_}≡ _ |-  _ => apply (discrete_iff _ _) in H
-  | H : _ ≡ _ |-  _ => apply leibniz_equiv in H
-  | _ => progress simplify_eq
-  end;
-  (* repeatedly apply congruence lemmas and use the equalities in the hypotheses. *)
-  try (f_equiv; fast_done || auto_equiv).
-
-Ltac solve_proper ::= (repeat intros ?; simpl; auto_equiv).
-
 Definition logN : namespace := nroot .@ "logN".
 
 (** interp : is a unary logical relation. *)
@@ -40,7 +23,7 @@ Section logrel.
 
   Definition interp_expr (τi : listO D -n> D) (Δ : listO D)
       (ee : expr * expr) : iProp Σ := (∀ j K,
-    j ⤇ fill K (ee.2) →
+    j ⤇ fill K (ee.2) -∗
     WP ee.1 {{ v, ∃ v', j ⤇ fill K (of_val v') ∗ τi Δ (v, v') }})%I.
   Global Instance interp_expr_ne n :
     Proper (dist n ==> dist n ==> (=) ==> dist n) interp_expr.
@@ -101,8 +84,8 @@ Section logrel.
   Program Definition interp_exist (interp : listO D -n> D) : listO D -n> D :=
     λne Δ,
     PersPred
-      (λ ww, □ ∃ (τi : D) vv, ⌜ww = (PackV vv.1, PackV vv.2)⌝ ∗
-                 interp (τi :: Δ) vv)%I.
+      (λ ww, ∃ (τi : D) vv, ⌜ww = (PackV vv.1, PackV vv.2)⌝ ∗
+               interp (τi :: Δ) vv)%I.
   Solve Obligations with repeat intros ?; simpl; solve_proper.
 
   Program Definition interp_rec1
@@ -174,20 +157,19 @@ Section logrel.
     ≡ ⟦ τ ⟧ (Δ1 ++ Δ2).
   Proof.
     revert Δ1 Π Δ2. induction τ=> Δ1 Π Δ2 vv; simpl; auto.
-    - properness; auto; match goal with IH : ∀ _, _ |- _ => by apply IH end.
-    - properness; auto; match goal with IH : ∀ _, _ |- _ => by apply IH end.
+    - by repeat (f_equiv; try match goal with IH : ∀ _, _ |- _ => by apply IH end).
+    - by repeat (f_equiv; try match goal with IH : ∀ _, _ |- _ => by apply IH end).
     - unfold interp_expr.
-      properness; auto; match goal with IH : ∀ _, _ |- _ => by apply IH end.
+      by repeat (f_equiv; try match goal with IH : ∀ _, _ |- _ => by apply IH end).
     - rewrite fixpoint_proper; first done. intros τi ww; simpl.
-      properness; auto.
-      match goal with IH : ∀ _, _ |- _ => by apply (IH (_ :: _)) end.
+      by repeat (f_equiv; try match goal with IH : ∀ _, _ |- _ => by apply (IH (_ :: _)) end).
     - rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl.
       { by rewrite !lookup_app_l. }
       rewrite !lookup_app_r; [|lia..]. do 3 f_equiv. lia.
     - unfold interp_expr.
-      properness; auto. match goal with IH : ∀ _, _ |- _ => by apply (IH (_ :: _)) end.
-    - properness; auto. match goal with IH : ∀ _, _ |- _ => by apply (IH (_ :: _)) end.
-    - properness; auto. match goal with IH : ∀ _, _ |- _ => by apply IH end.
+      by repeat (f_equiv; try match goal with IH : ∀ _, _ |- _ => by apply (IH (_ :: _)) end).
+    - by repeat (f_equiv; try match goal with IH : ∀ _, _ |- _ => by apply (IH (_ :: _)) end).
+    - by repeat (f_equiv; try match goal with IH : ∀ _, _ |- _ => by apply IH end).
   Qed.
 
   Lemma interp_subst_up Δ1 Δ2 τ τ' :
@@ -195,12 +177,12 @@ Section logrel.
     ≡ ⟦ τ.[upn (length Δ1) (τ' .: ids)] ⟧ (Δ1 ++ Δ2).
   Proof.
     revert Δ1 Δ2; induction τ=> Δ1 Δ2 vv; simpl; auto.
-    - properness; auto; match goal with IH : ∀ _, _ |- _ => by apply IH end.
-    - properness; auto; match goal with IH : ∀ _, _ |- _ => by apply IH end.
+    - by repeat (f_equiv; try match goal with IH : ∀ _, _ |- _ => by apply IH end).
+    - by repeat (f_equiv; try match goal with IH : ∀ _, _ |- _ => by apply IH end).
     - unfold interp_expr.
-      properness; auto; match goal with IH : ∀ _, _ |- _ => by apply IH end.
+      by repeat (f_equiv; try match goal with IH : ∀ _, _ |- _ => by apply IH end).
     - rewrite fixpoint_proper; first done; intros τi ww; simpl.
-      properness; auto. match goal with IH : ∀ _, _ |- _ => by apply (IH (_ :: _)) end.
+      by repeat (f_equiv; try match goal with IH : ∀ _, _ |- _ => by apply (IH (_ :: _)) end).
     - match goal with |- context [_ !! ?x] => rename x into idx end.
       rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl.
       { by rewrite !lookup_app_l. }
@@ -209,9 +191,9 @@ Section logrel.
       { symmetry. asimpl. apply (interp_weaken [] Δ1 Δ2 τ'). }
       rewrite !lookup_app_r; [|lia ..]. do 3 f_equiv. lia.
     - unfold interp_expr.
-      properness; auto. match goal with IH : ∀ _, _ |- _ => by apply (IH (_ :: _)) end.
-    - properness; auto. match goal with IH : ∀ _, _ |- _ => by apply (IH (_ :: _)) end.
-    - properness; auto. match goal with IH : ∀ _, _ |- _ => by apply IH end.
+      by repeat (f_equiv; try match goal with IH : ∀ _, _ |- _ => by apply (IH (_ :: _)) end).
+    - by repeat (f_equiv; try match goal with IH : ∀ _, _ |- _ => by apply (IH (_ :: _)) end).
+    - by repeat (f_equiv; try match goal with IH : ∀ _, _ |- _ => by apply IH end).
   Qed.
 
   Lemma interp_subst Δ2 τ τ' v : ⟦ τ ⟧ (⟦ τ' ⟧ Δ2 :: Δ2) v ≡ ⟦ τ.[τ'/] ⟧ Δ2 v.
@@ -248,131 +230,55 @@ Section logrel.
     apply sep_proper; auto. apply (interp_weaken [] [τi] Δ).
   Qed.
 
-  Lemma interp_ref_pointsto_neq E Δ τ l w (l1 l2 l3 l4 : loc) :
-    ↑logN.@(l1, l2) ⊆ E →
-    l2 ≠ l4 →
-    l ↦ᵢ w -∗ interp (Tref τ) Δ (LocV l1, LocV l2) -∗
-      |={E ∖ ↑logN.@(l3, l4)}=> l ↦ᵢ w ∗ ⌜l ≠ l1⌝.
-  Proof.
-    intros Hnin Hneq.
-    destruct (decide (l = l1)); subst; last auto.
-    iIntros "Hl1"; simpl; iDestruct 1 as ((l5, l6)) "[% Hl2]"; simplify_eq.
-    iInv (logN.@(l5, l6)) as "Hi" "Hcl"; simpl.
-    iDestruct "Hi" as ((v1, v2))  "(Hl3 & Hl2' & ?)".
-    iMod "Hl3".
-    by iDestruct (@mapsto_valid_2 with "Hl1 Hl3") as %[??].
-  Qed.
-
-  Lemma interp_ref_pointsto_neq' E Δ τ l w (l1 l2 l3 l4 : loc) :
-    ↑logN.@(l1, l2) ⊆ E →
-    l1 ≠ l3 →
-    l ↦ₛ w -∗ interp (Tref τ) Δ (LocV l1, LocV l2) -∗
-      |={E ∖ ↑logN.@(l3, l4)}=> l ↦ₛ w ∗ ⌜l ≠ l2⌝.
-  Proof.
-    intros Hnin Hneq.
-    destruct (decide (l = l2)); subst; last auto.
-    iIntros "Hl1"; simpl; iDestruct 1 as ((l5, l6)) "[% Hl2]"; simplify_eq.
-    iInv (logN.@(l5, l6)) as "Hi" "Hcl"; simpl.
-    iDestruct "Hi" as ((v1, v2)) "(Hl3 & >Hl2' & ?)".
-    by iDestruct (mapstoS_valid_2 with "Hl1 Hl2'") as %[].
-  Qed.
-
-  Lemma interp_ref_open' Δ τ l l' :
+  Lemma interp_EqType_one_to_one Δ τ l l' u u' v v' w w' :
     EqType τ →
-    ⟦ Tref τ ⟧ Δ (LocV l, LocV l') -∗
-               |={⊤, ⊤ ∖ ↑logN.@(l, l')}=>
-  ∃ w w', ▷ l ↦ᵢ w ∗ ▷ l' ↦ₛ w' ∗ ▷ ⟦ τ ⟧ Δ (w, w') ∗
-            ▷ (∀ z z' u u' v v',
-                  l ↦ᵢ z -∗ l' ↦ₛ z' -∗ ⟦ τ ⟧ Δ (u, u') -∗ ⟦ τ ⟧ Δ (v, v') -∗
-                    |={⊤ ∖ ↑logN.@(l, l')}=> l ↦ᵢ z ∗
-                                              l' ↦ₛ z' ∗ ⌜v = u ↔ v' = u'⌝)
-            ∗ (▷ (∃ vv : val * val, l ↦ᵢ vv.1 ∗ l' ↦ₛ vv.2 ∗ ⟦ τ ⟧ Δ vv)
-          ={⊤ ∖ ↑logN.@(l, l'), ⊤}=∗ True).
+    l ↦ᵢ u -∗
+    l' ↦ₛ u' -∗
+    ⟦ τ ⟧ Δ (v, v') -∗
+    ⟦ τ ⟧ Δ (w, w') ={⊤ ∖ ↑logN.@(l, l')}=∗
+    l ↦ᵢ u ∗ l' ↦ₛ u' ∗ ⌜v = w ↔ v' = w'⌝.
   Proof.
-    iIntros (Heqt); simpl.
-    iDestruct 1 as ((l1, l1')) "[% H1]"; simplify_eq.
-    iInv (logN.@(l1, l1')) as "Hi" "$"; simpl.
-    iDestruct "Hi" as ((v1, v2))  "(Hl1 & Hl1' & Hrl)"; simpl in *.
-    destruct Heqt; simpl in *.
-    - iModIntro; iExists _, _; iFrame.
-      iNext. iIntros (??????) "? ?". iIntros ([??] [??]); subst.
-      by iModIntro; iFrame.
-    - iModIntro; iExists _, _; iFrame.
-      iNext. iIntros (??????) "? ?".
-      iDestruct 1 as (?) "[% %]". iDestruct 1 as (?) "[% %]".
-      simplify_eq. by iModIntro; iFrame.
-    - iModIntro; iExists _, _; iFrame.
-      iNext. iIntros (??????) "? ?".
-      iDestruct 1 as (?) "[% %]". iDestruct 1 as (?) "[% %]".
-      simplify_eq. by iModIntro; iFrame.
-    - iModIntro; iExists _, _; iFrame; iFrame "#". iNext.
-      iIntros (z z' u u' v v') "Hl1 Hl1' Huu". iDestruct 1 as ((l2, l2')) "[% #Hl2]";
-        simplify_eq; simpl in *.
-      iDestruct "Huu" as ((l3, l3')) "[% #Hl3]";
-        simplify_eq; simpl in *.
-      destruct (decide ((l1, l1') = (l2, l2'))); simplify_eq.
-      + destruct (decide ((l2, l2') = (l3, l3'))); simplify_eq; first by iFrame.
-        destruct (decide (l2 = l3)); destruct (decide (l2' = l3')); subst.
-        * iMod (interp_ref_pointsto_neq with "Hl1 []")
-               as "[Hl1 %]"; simpl; eauto.
-             by iFrame.
-        * iMod (interp_ref_pointsto_neq with "Hl1 []")
-               as "[Hl1 %]"; simpl; eauto.
-             { by iExists (_, _); iFrame "#". }
-             by iFrame.
-        * iMod (interp_ref_pointsto_neq' with "Hl1' []")
-               as "[Hl1' %]";
-               simpl; eauto.
-             { by iExists (_, _); iFrame "#". }
-             by iFrame.
-        * iFrame; iModIntro; iPureIntro; split; by inversion 1.
-      + destruct (decide ((l1, l1') = (l3, l3'))); simplify_eq.
-        * destruct (decide (l2 = l3)); destruct (decide (l2' = l3')); subst.
-          -- iMod (interp_ref_pointsto_neq with "Hl1 []")
-              as "[Hl1 %]"; simpl; eauto.
-             by iFrame.
-          -- iMod (interp_ref_pointsto_neq with "Hl1 []")
-               as "[Hl1 %]"; simpl; eauto.
-             { iExists (_, _); iSplit; first eauto. iFrame "#". }
-             by iFrame.
-          -- iMod (interp_ref_pointsto_neq' with "Hl1' []")
-               as "[Hl1' %]";
-               simpl; eauto.
-             { iExists (_, _); iSplit; first eauto. iFrame "#". }
-             by iFrame.
-          -- iFrame; iModIntro; iPureIntro; split; by inversion 1.
-        * destruct (decide ((l2, l2') = (l3, l3'))); simplify_eq.
-          -- destruct (decide (l1 = l3)); destruct (decide (l1' = l3')); subst.
-             ++ iMod (interp_ref_pointsto_neq with "Hl1 []")
-                 as "[Hl1 %]"; simpl; eauto.
-                by iFrame.
-             ++ iMod (interp_ref_pointsto_neq with "Hl1 []")
-               as "[Hl1 %]"; simpl; eauto.
-                { by iExists (_, _); iFrame "#". }
-                  by iFrame.
-             ++ iMod (interp_ref_pointsto_neq' with "Hl1' []")
-                 as "[Hl1' %]";
-                  simpl; eauto.
-                { by iExists (_, _); iFrame "#". }
-                  by iFrame.
-             ++ iFrame; iModIntro; iPureIntro; split; by inversion 1.
-          -- iFrame.
-             { destruct (decide (l2 = l3)); destruct (decide (l2' = l3'));
-                 simplify_eq; auto.
-               + iInv (logN.@(l3, l2')) as "Hib1" "Hcl1".
-                 iInv (logN.@(l3, l3')) as "Hib2" "Hcl2".
-                 iDestruct "Hib1" as ((v11, v12)) "(Hlx1' & Hlx2 & Hr1)".
-                 iDestruct "Hib2" as ((v11', v12')) "(Hl1'' & Hl2' & Hr2)".
-                 simpl.
-                 iMod "Hlx1'"; iMod "Hl1''".
-                   by iDestruct (@mapsto_valid_2 with "Hlx1' Hl1''") as %[??].
-               + iInv (logN.@(l2, l3')) as "Hib1" "Hcl1".
-                 iInv (logN.@(l3, l3')) as "Hib2" "Hcl2".
-                 iDestruct "Hib1" as ((v11, v12)) "(>Hl1 & >Hl2' & Hr1)".
-                 iDestruct "Hib2" as ((v11', v12')) "(>Hl1' & >Hl2'' & Hr2) /=".
-                 by iDestruct (mapstoS_valid_2 with "Hl2' Hl2''") as %[].
-               + iModIntro; iPureIntro; split; intros; simplify_eq. }
+    iIntros (Heqt) "Hl Hl' Hvv Hww".
+    destruct τ; inversion Heqt; simplify_eq/=.
+    { iDestruct "Hvv"as "[% %]"; simplify_eq.
+      iDestruct "Hww"as "[% %]"; simplify_eq.
+      by iFrame. }
+    { iDestruct "Hvv"as "(%&%&%)"; simplify_eq.
+      iDestruct "Hww"as "(%&%&%)"; simplify_eq.
+      by iFrame. }
+    { iDestruct "Hvv"as "(%&%&%)"; simplify_eq.
+      iDestruct "Hww"as "(%&%&%)"; simplify_eq.
+      by iFrame. }
+    iDestruct "Hvv"as ([l1 l1']) "[% Hll1]"; simplify_eq.
+    iDestruct "Hww"as ([l2 l2']) "[% Hll2]"; simplify_eq.
+    simpl.
+    destruct (decide (l1 = l)); simplify_eq.
+    - destruct (decide (l1' = l')); simplify_eq.
+      + destruct (decide (l2 = l)); simplify_eq.
+        * destruct (decide (l2' = l')); simplify_eq; first by iFrame.
+          iInv (logN.@(l, l2')) as ([v v']) "(>Hlx & >Hlx' & Hvv) /=" "Hclose".
+          iDestruct (mapsto_valid_2 with "Hl Hlx") as %[? ?]; done.
+        * destruct (decide (l2' = l')); simplify_eq; last first.
+          { iModIntro; iFrame; iPureIntro; intuition simplify_eq. }
+          iInv (logN.@(l2, l')) as ([v v']) "(>Hlx & >Hlx' & Hvv) /=" "Hclose".
+          iDestruct (mapstoS_valid_2 with "Hl' Hlx'") as %?; done.
+      + iInv (logN.@(l, l1')) as ([v v']) "(>Hlx & >Hlx' & Hvv) /=" "Hclose".
+          iDestruct (mapsto_valid_2 with "Hl Hlx") as %[? ?]; done.
+    - destruct (decide (l1 = l2)); simplify_eq.
+      + destruct (decide (l1' = l2')); simplify_eq; first by iFrame.
+        iInv (logN.@(l2, l1')) as ([v v']) "(>Hlx & >Hlx' & Hvv) /=" "Hclose".
+        iInv (logN.@(l2, l2')) as ([w w']) "(>Hly & >Hly' & Hww) /=" "Hclose'".
+        iDestruct (mapsto_valid_2 with "Hly Hlx") as %[? ?]; done.
+      + destruct (decide (l1' = l2')); simplify_eq; last first.
+        { iModIntro; iFrame; iPureIntro; intuition simplify_eq. }
+        destruct (decide (l2' = l')); simplify_eq.
+        * iInv (logN.@(l1, l')) as ([v v']) "(>Hlx & >Hlx' & Hvv) /=" "Hclose".
+          iDestruct (mapstoS_valid_2 with "Hl' Hlx'") as %?; done.
+        * iInv (logN.@(l1, l2')) as ([v v']) "(>Hlx & >Hlx' & Hvv) /=" "Hclose".
+          iInv (logN.@(l2, l2')) as ([w w']) "(>Hly & >Hly' & Hww) /=" "Hclose'".
+          iDestruct (mapstoS_valid_2 with "Hly' Hlx'") as %?; done.
   Qed.
+
 End logrel.
 
 Global Typeclasses Opaque interp_env.
diff --git a/theories/logrel/F_mu_ref_conc/unary/examples/symbol_nat.v b/theories/logrel/F_mu_ref_conc/unary/examples/symbol_nat.v
index 0447470bf0484dfa1e3ffaee153cb9325037e401..aa06206f38261627bdda3d3e6937691df8c5a61c 100644
--- a/theories/logrel/F_mu_ref_conc/unary/examples/symbol_nat.v
+++ b/theories/logrel/F_mu_ref_conc/unary/examples/symbol_nat.v
@@ -70,7 +70,6 @@ Section symbol_nat_sem_typ.
             with "[Hl Hmt]") as "#Hinv".
     { unfold Max_token. by iNext; iExists _; iFrame. }
     iApply wp_value.
-    iModIntro.
     iExists (PersPred (λ v, ∃ m, ⌜v = #nv m⌝ ∗ Token γ m))%I; simpl.
     iExists _; iSplit; first done.
     iExists _, _; iSplit; first done.
diff --git a/theories/logrel/F_mu_ref_conc/unary/fundamental.v b/theories/logrel/F_mu_ref_conc/unary/fundamental.v
index fa23ca40ab4362ca556bb5fe27c3e652a8f66482..559a3a2f471823e4f01db272f057d1aa5d688977 100644
--- a/theories/logrel/F_mu_ref_conc/unary/fundamental.v
+++ b/theories/logrel/F_mu_ref_conc/unary/fundamental.v
@@ -13,11 +13,9 @@ Section typed_interp.
   Context `{heapIG Σ}.
   Notation D := (persistent_predO val (iPropI Σ)).
 
-  Local Tactic Notation "smart_wp_bind"
-        uconstr(ctx) ident(v) constr(Hv) uconstr(Hp) :=
-    iApply (wp_bind (fill [ctx]));
-    iApply (wp_wand with "[-]"); [iApply Hp; trivial|]; cbn;
-    iIntros (v) Hv.
+  Lemma interp_expr_bind K e Δ τ τ' :
+    ⟦ τ ⟧ₑ Δ e -∗ (∀ v, ⟦ τ ⟧ Δ v -∗ ⟦ τ' ⟧ₑ Δ (fill K (of_val v))) -∗ ⟦ τ' ⟧ₑ Δ (fill K e).
+  Proof. iIntros; iApply wp_bind; iApply (wp_wand with "[$]"); done. Qed.
 
   Lemma sem_typed_var Γ x τ :
     Γ !! x = Some τ → ⊢ Γ ⊨ Var x : τ.
@@ -41,37 +39,40 @@ Section typed_interp.
     Γ ⊨ e1 : TNat -∗ Γ ⊨ e2 : TNat -∗ Γ ⊨ BinOp op e1 e2 : binop_res_type op.
   Proof.
     iIntros "#IH1 #IH2" (Δ vs) "!# #HΓ /=".
-    smart_wp_bind (BinOpLCtx _ e2.[env_subst vs]) v "#Hv" "IH1".
-    smart_wp_bind (BinOpRCtx _ v) v' "# Hv'" "IH2".
-    iDestruct "Hv" as (n) "%"; iDestruct "Hv'" as (n') "%"; simplify_eq/=.
+    iApply (interp_expr_bind [BinOpLCtx _ _]); first by iApply "IH1".
+    iIntros (v) "#Hv /=".
+    iApply (interp_expr_bind [BinOpRCtx _ _]); first by iApply "IH2".
+    iIntros (w) "#Hw/=".
+    iDestruct "Hv" as (n) "%"; iDestruct "Hw" as (n') "%"; simplify_eq/=.
     iApply wp_pure_step_later; [done|]; iIntros "!> _". iApply wp_value.
     destruct op; simpl; try destruct eq_nat_dec;
       try destruct le_dec; try destruct lt_dec; eauto 10.
   Qed.
 
-  Lemma sem_typed_pair Γ e1 e2 τ1 τ2 :
-    Γ ⊨ e1 : τ1 -∗ Γ ⊨ e2 : τ2 -∗ Γ ⊨ Pair e1 e2 : TProd τ1 τ2.
+  Lemma sem_typed_pair Γ e1 e2 τ1 τ2 : Γ ⊨ e1 : τ1 -∗ Γ ⊨ e2 : τ2 -∗ Γ ⊨ Pair e1 e2 : TProd τ1 τ2.
   Proof.
     iIntros "#IH1 #IH2" (Δ vs) "!# #HΓ"; simpl.
-    smart_wp_bind (PairLCtx e2.[env_subst vs]) v "#Hv" "IH1".
-    smart_wp_bind (PairRCtx v) v' "# Hv'" "IH2".
-    iApply wp_value; eauto.
+    iApply (interp_expr_bind [PairLCtx _]); first by iApply "IH1".
+    iIntros (v) "#Hv /=".
+    iApply (interp_expr_bind [PairRCtx _]); first by iApply "IH2".
+    iIntros (w) "#Hw/=".
+    iApply wp_value; simpl; eauto.
   Qed.
 
-  Lemma sem_typed_fst Γ e τ1 τ2 :
-        Γ ⊨ e : TProd τ1 τ2 -∗ Γ ⊨ Fst e : τ1.
+  Lemma sem_typed_fst Γ e τ1 τ2 : Γ ⊨ e : TProd τ1 τ2 -∗ Γ ⊨ Fst e : τ1.
   Proof.
     iIntros "#IH" (Δ vs) "!# #HΓ"; simpl.
-    smart_wp_bind (FstCtx) v "# Hv" "IH"; cbn.
+    iApply (interp_expr_bind [FstCtx]); first by iApply "IH".
+    iIntros (v) "#Hv /=".
     iDestruct "Hv" as (w1 w2) "#[% [H2 H3]]"; subst.
     iApply wp_pure_step_later; [done|]; iIntros "!> _". by iApply wp_value.
   Qed.
 
-  Lemma sem_typed_snd Γ e τ1 τ2 :
-    Γ ⊨ e : TProd τ1 τ2 -∗ Γ ⊨ Snd e : τ2.
+  Lemma sem_typed_snd Γ e τ1 τ2 : Γ ⊨ e : TProd τ1 τ2 -∗ Γ ⊨ Snd e : τ2.
   Proof.
     iIntros "#IH" (Δ vs) "!# #HΓ"; simpl.
-    smart_wp_bind (SndCtx) v "# Hv" "IH"; cbn.
+    iApply (interp_expr_bind [SndCtx]); first by iApply "IH".
+    iIntros (v) "#Hv /=".
     iDestruct "Hv" as (w1 w2) "#[% [H2 H3]]"; subst.
     iApply wp_pure_step_later; [done|]; iIntros "!> _". by iApply wp_value.
   Qed.
@@ -79,15 +80,17 @@ Section typed_interp.
   Lemma sem_typed_injl Γ e τ1 τ2 : Γ ⊨ e : τ1 -∗ Γ ⊨ InjL e : (TSum τ1 τ2).
   Proof.
     iIntros "#IH" (Δ vs) "!# #HΓ"; simpl.
-    smart_wp_bind (InjLCtx) v "# Hv" "IH"; cbn.
-    iApply wp_value; eauto.
+    iApply (interp_expr_bind [InjLCtx]); first by iApply "IH".
+    iIntros (v) "#Hv /=".
+    iApply wp_value; simpl; eauto.
   Qed.
 
   Lemma sem_typed_injr Γ e τ1 τ2 : Γ ⊨ e : τ2 -∗ Γ ⊨ InjR e : TSum τ1 τ2.
   Proof.
     iIntros "#IH" (Δ vs) "!# #HΓ"; simpl.
-    smart_wp_bind (InjRCtx) v "# Hv" "IH"; cbn.
-    iApply wp_value; eauto.
+    iApply (interp_expr_bind [InjRCtx]); first by iApply "IH".
+    iIntros (v) "#Hv /=".
+    iApply wp_value; simpl; eauto.
   Qed.
 
   Lemma sem_typed_case Γ e0 e1 e2 τ1 τ2 τ3 :
@@ -97,7 +100,8 @@ Section typed_interp.
     Γ ⊨ Case e0 e1 e2 : τ3.
   Proof.
     iIntros "#IH1 #IH2 #IH3" (Δ vs) "!# #HΓ"; simpl.
-    smart_wp_bind (CaseCtx _ _) v "#Hv" "IH1"; cbn.
+    iApply (interp_expr_bind [CaseCtx _ _]); first by iApply "IH1".
+    iIntros (v) "#Hv /=".
     iDestruct (interp_env_length with "HΓ") as %?.
     iDestruct "Hv" as "[Hv|Hv]"; iDestruct "Hv" as (w) "[% Hw]"; simplify_eq/=.
     + iApply wp_pure_step_later; auto 1 using to_of_val; asimpl. iIntros "!> _".
@@ -110,7 +114,8 @@ Section typed_interp.
     Γ ⊨ e0 : TBool -∗ Γ ⊨ e1 : τ -∗ Γ ⊨ e2 : τ -∗ Γ ⊨ If e0 e1 e2 : τ.
   Proof.
     iIntros "#IH1 #IH2 #IH3" (Δ vs) "!# #HΓ"; simpl.
-    smart_wp_bind (IfCtx _ _) v "#Hv" "IH1"; cbn.
+    iApply (interp_expr_bind [IfCtx _ _]); first by iApply "IH1".
+    iIntros (v) "#Hv /=".
     iDestruct "Hv" as ([]) "%"; subst; simpl;
       [iApply wp_pure_step_later .. ]; auto; iIntros "!> _";
         [iApply "IH2"| iApply "IH3"]; auto.
@@ -139,37 +144,37 @@ Section typed_interp.
     iApply interp_env_cons; iSplit; auto.
   Qed.
 
-  Lemma sem_typed_letin Γ e1 e2 τ1 τ2 :
-    Γ ⊨ e1 : τ1 -∗ τ1 :: Γ ⊨ e2 : τ2 -∗ Γ ⊨ LetIn e1 e2: τ2.
+  Lemma sem_typed_letin Γ e1 e2 τ1 τ2 : Γ ⊨ e1 : τ1 -∗ τ1 :: Γ ⊨ e2 : τ2 -∗ Γ ⊨ LetIn e1 e2: τ2.
   Proof.
     iIntros "#IH1 #IH2" (Δ vs) "!# #HΓ"; simpl.
-    smart_wp_bind (LetInCtx _) v "#Hv" "IH1"; cbn.
+    iApply (interp_expr_bind [LetInCtx _]); first by iApply "IH1".
+    iIntros (v) "#Hv /=".
     iDestruct (interp_env_length with "HΓ") as %?.
     iApply wp_pure_step_later; auto 1 using to_of_val. iIntros "!> _".
     asimpl. iApply ("IH2" $! Δ (v :: vs)).
     iApply interp_env_cons; iSplit; eauto.
   Qed.
 
-  Lemma sem_typed_seq Γ e1 e2 τ1 τ2 :
-    Γ ⊨ e1 : τ1 -∗ Γ ⊨ e2 : τ2 -∗ Γ ⊨ Seq e1 e2 : τ2.
+  Lemma sem_typed_seq Γ e1 e2 τ1 τ2 : Γ ⊨ e1 : τ1 -∗ Γ ⊨ e2 : τ2 -∗ Γ ⊨ Seq e1 e2 : τ2.
   Proof.
     iIntros "#IH1 #IH2" (Δ vs) "!# #HΓ"; simpl.
-    smart_wp_bind (SeqCtx _) v "#Hv" "IH1"; cbn.
+    iApply (interp_expr_bind [SeqCtx _]); first by iApply "IH1".
+    iIntros (v) "#Hv /=".
     iApply wp_pure_step_later; auto 1 using to_of_val. iIntros "!> _".
     iApply "IH2"; done.
   Qed.
 
-  Lemma sem_typed_app Γ e1 e2 τ1 τ2 :
-      Γ ⊨ e1 : TArrow τ1 τ2 -∗ Γ ⊨ e2 : τ1 -∗ Γ ⊨ App e1 e2 :  τ2.
+  Lemma sem_typed_app Γ e1 e2 τ1 τ2 : Γ ⊨ e1 : TArrow τ1 τ2 -∗ Γ ⊨ e2 : τ1 -∗ Γ ⊨ App e1 e2 :  τ2.
   Proof.
     iIntros "#IH1 #IH2" (Δ vs) "!# #HΓ"; simpl.
-    smart_wp_bind (AppLCtx (e2.[env_subst vs])) v "#Hv" "IH1".
-    smart_wp_bind (AppRCtx v) w "#Hw" "IH2".
+    iApply (interp_expr_bind [AppLCtx _]); first by iApply "IH1".
+    iIntros (v) "#Hv /=".
+    iApply (interp_expr_bind [AppRCtx _]); first by iApply "IH2".
+    iIntros (w) "#Hw/=".
     iApply "Hv"; done.
   Qed.
 
-  Lemma sem_typed_tlam Γ e τ :
-    (subst (ren (+1)) <$> Γ) ⊨ e : τ -∗ Γ ⊨ TLam e : TForall τ.
+  Lemma sem_typed_tlam Γ e τ : (subst (ren (+1)) <$> Γ) ⊨ e : τ -∗ Γ ⊨ TLam e : TForall τ.
   Proof.
     iIntros "#IH" (Δ vs) "!# #HΓ /=".
     iApply wp_value; simpl.
@@ -180,7 +185,8 @@ Section typed_interp.
   Lemma sem_typed_tapp Γ e τ τ' : Γ ⊨ e : TForall τ -∗ Γ ⊨ TApp e : τ.[τ'/].
   Proof.
     iIntros "#IH" (Δ vs) "!# #HΓ /=".
-    smart_wp_bind TAppCtx v "#Hv" "IH"; cbn.
+    iApply (interp_expr_bind [TAppCtx]); first by iApply "IH".
+    iIntros (v) "#Hv /=".
     iApply wp_wand_r; iSplitL;
       [iApply ("Hv" $! (⟦ τ' ⟧ Δ)); iPureIntro; apply _|]; cbn.
     iIntros (w) "?". by iApply interp_subst.
@@ -189,9 +195,11 @@ Section typed_interp.
   Lemma sem_typed_pack Γ e τ τ' : Γ ⊨ e : τ.[τ'/] -∗ Γ ⊨ Pack e : TExist τ.
   Proof.
     iIntros "#IH" (Δ vs) "!##HΓ /=".
-    smart_wp_bind PackCtx v "#Hv" "IH". iApply wp_value.
+    iApply (interp_expr_bind [PackCtx]); first by iApply "IH".
+    iIntros (v) "#Hv /=".
+    iApply wp_value.
     rewrite -interp_subst.
-    iExists (interp _ Δ), _; iModIntro; iSplit; done.
+    iExists (interp _ Δ), _; iSplit; done.
   Qed.
 
   Lemma sem_typed_unpack Γ e1 e2 τ τ' :
@@ -200,7 +208,8 @@ Section typed_interp.
     Γ ⊨ UnpackIn e1 e2 : τ'.
   Proof.
     iIntros "#IH1 #IH2" (Δ vs) "!# #HΓ /=".
-    smart_wp_bind (UnpackInCtx _) v "#Hv" "IH1".
+    iApply (interp_expr_bind [UnpackInCtx _]); first by iApply "IH1".
+    iIntros (v) "#Hv /=".
     iDestruct "Hv" as (τi w ->) "#Hw"; simpl.
     iApply wp_pure_step_later; auto 1 using to_of_val. iIntros "!> _".
     asimpl.
@@ -215,7 +224,9 @@ Section typed_interp.
   Lemma sem_typed_fold Γ e τ : Γ ⊨ e : τ.[(TRec τ)/] -∗ Γ ⊨ Fold e : TRec τ.
   Proof.
     iIntros "#IH" (Δ vs) "!# #HΓ /=".
-    smart_wp_bind FoldCtx v "#Hv" ("IH" $! Δ vs). iApply wp_value.
+    iApply (interp_expr_bind [FoldCtx]); first by iApply "IH".
+    iIntros (v) "#Hv /=".
+    iApply wp_value.
     rewrite /= -interp_subst fixpoint_interp_rec1_eq /=.
     iModIntro; eauto.
   Qed.
@@ -223,7 +234,8 @@ Section typed_interp.
   Lemma sem_typed_unfold Γ e τ : Γ ⊨ e : TRec τ -∗ Γ ⊨ Unfold e : τ.[(TRec τ)/].
   Proof.
     iIntros "#IH" (Δ vs) "!# #HΓ /=".
-    smart_wp_bind UnfoldCtx v "#Hv" ("IH" $! Δ vs).
+    iApply (interp_expr_bind [UnfoldCtx]); first by iApply "IH".
+    iIntros (v) "#Hv /=".
     rewrite /= fixpoint_interp_rec1_eq.
     change (fixpoint _) with (⟦ TRec τ ⟧ Δ); simpl.
     iDestruct "Hv" as (w) "#[% Hw]"; subst.
@@ -241,9 +253,11 @@ Section typed_interp.
   Lemma sem_typed_alloc Γ e τ : Γ ⊨ e : τ -∗ Γ ⊨ Alloc e : Tref τ.
   Proof.
     iIntros "#IH" (Δ vs) "!# #HΓ /=".
-    smart_wp_bind AllocCtx v "#Hv" "IH"; cbn. iClear "HΓ". iApply wp_fupd.
+    iApply (interp_expr_bind [AllocCtx]); first by iApply "IH".
+    iIntros (v) "#Hv /=".
+    iApply wp_fupd.
     iApply wp_alloc; auto 1 using to_of_val.
-    iNext; iIntros (l) "Hl".
+    iNext; iIntros (l) "Hl /=".
     iMod (inv_alloc _ with "[Hl]") as "HN";
       [| iModIntro; iExists _; iSplit; trivial]; eauto.
   Qed.
@@ -251,7 +265,8 @@ Section typed_interp.
   Lemma sem_typed_load Γ e τ : Γ ⊨ e : (Tref τ) -∗ Γ ⊨ Load e : τ.
   Proof.
     iIntros "#IH" (Δ vs) "!# #HΓ /=".
-    smart_wp_bind LoadCtx v "#Hv" "IH"; cbn. iClear "HΓ".
+    iApply (interp_expr_bind [LoadCtx]); first by iApply "IH".
+    iIntros (v) "#Hv /=".
     iDestruct "Hv" as (l) "[% #Hv]"; subst.
     iApply wp_atomic.
     iInv (logN .@ l) as (w) "[Hw1 #Hw2]" "Hclose".
@@ -260,12 +275,13 @@ Section typed_interp.
     iIntros "Hw1". iMod ("Hclose" with "[Hw1 Hw2]"); eauto.
   Qed.
 
-  Lemma sem_typed_store Γ e1 e2 τ :
-    Γ ⊨ e1 : (Tref τ) -∗ Γ ⊨ e2 : τ -∗ Γ ⊨ Store e1 e2 : TUnit.
+  Lemma sem_typed_store Γ e1 e2 τ : Γ ⊨ e1 : (Tref τ) -∗ Γ ⊨ e2 : τ -∗ Γ ⊨ Store e1 e2 : TUnit.
   Proof.
     iIntros "#IH1 #IH2" (Δ vs) "!# #HΓ /=".
-    smart_wp_bind (StoreLCtx _) v "#Hv" "IH1"; cbn.
-    smart_wp_bind (StoreRCtx _) w "#Hw" "IH2"; cbn. iClear "HΓ".
+    iApply (interp_expr_bind [StoreLCtx _]); first by iApply "IH1".
+    iIntros (v) "#Hv /=".
+    iApply (interp_expr_bind [StoreRCtx _]); first by iApply "IH2".
+    iIntros (w) "#Hw/=".
     iDestruct "Hv" as (l) "[% #Hv]"; subst.
     iApply wp_atomic.
     iInv (logN .@ l) as (z) "[Hz1 #Hz2]" "Hclose".
@@ -283,9 +299,12 @@ Section typed_interp.
   Proof.
     iIntros (Heqτ) "#IH1 #IH2 #IH3".
     iIntros (Δ vs) "!# #HΓ /=".
-    smart_wp_bind (CasLCtx _ _) v1 "#Hv1" "IH1"; cbn.
-    smart_wp_bind (CasMCtx _ _) v2 "#Hv2" "IH2"; cbn.
-    smart_wp_bind (CasRCtx _ _) v3 "#Hv3" "IH3"; cbn. iClear "HΓ".
+    iApply (interp_expr_bind [CasLCtx _ _]); first by iApply "IH1".
+    iIntros (v1) "#Hv1 /=".
+    iApply (interp_expr_bind [CasMCtx _ _]); first by iApply "IH2".
+    iIntros (v2) "#Hv2 /=".
+    iApply (interp_expr_bind [CasRCtx _ _]); first by iApply "IH3".
+    iIntros (v3) "#Hv3 /=".
     iDestruct "Hv1" as (l) "[% Hv1]"; subst.
     iApply wp_atomic.
     iInv (logN .@ l) as (w) "[Hw1 #Hw2]" "Hclose".
@@ -298,12 +317,13 @@ Section typed_interp.
       iIntros "Hw1". iMod ("Hclose" with "[Hw1 Hw2]"); eauto.
   Qed.
 
-  Lemma sem_typed_FAA Γ e1 e2 :
-    Γ ⊨ e1 : Tref TNat -∗ Γ ⊨ e2 : TNat -∗ Γ ⊨ FAA e1 e2 : TNat.
+  Lemma sem_typed_FAA Γ e1 e2 : Γ ⊨ e1 : Tref TNat -∗ Γ ⊨ e2 : TNat -∗ Γ ⊨ FAA e1 e2 : TNat.
   Proof.
     iIntros "#IH1 #IH2" (Δ vs) "!# #HΓ /=".
-    smart_wp_bind (FAALCtx _) v1 "#Hv1" "IH1"; cbn.
-    smart_wp_bind (FAARCtx _) v2 "#Hv2" "IH2"; cbn. iClear "HΓ".
+    iApply (interp_expr_bind [FAALCtx _]); first by iApply "IH1".
+    iIntros (v1) "#Hv1 /=".
+    iApply (interp_expr_bind [FAARCtx _]); first by iApply "IH2".
+    iIntros (v2) "#Hv2 /=".
     iDestruct "Hv1" as (l) "[% Hv1]".
     iDestruct "Hv2" as (k) "%"; simplify_eq/=.
     iApply wp_atomic.
diff --git a/theories/logrel/F_mu_ref_conc/unary/logrel.v b/theories/logrel/F_mu_ref_conc/unary/logrel.v
index 3b642cb7a185b1e4b66dd5f30175a149e6c7a9dd..ac3b6fa2cc7051735ccff67b242a16566b94d3df 100644
--- a/theories/logrel/F_mu_ref_conc/unary/logrel.v
+++ b/theories/logrel/F_mu_ref_conc/unary/logrel.v
@@ -56,7 +56,7 @@ Section logrel.
   Solve Obligations with repeat intros ?; simpl; solve_proper.
 
   Program Definition interp_exist (interp : listO D -n> D) : listO D -n> D :=
-    λne Δ, PersPred (λ w, □ ∃ (τi : D) v, ⌜w = PackV v⌝ ∗ interp (τi :: Δ) v)%I.
+    λne Δ, PersPred (λ w, ∃ (τi : D) v, ⌜w = PackV v⌝ ∗ interp (τi :: Δ) v)%I.
   Solve Obligations with repeat intros ?; simpl; solve_proper.
 
   Definition interp_rec1 (interp : listO D -n> D) (Δ : listO D) (τi : D) : D :=
@@ -120,56 +120,42 @@ Section logrel.
     ⟦ τ.[upn (length Δ1) (ren (+ length Π))] ⟧ (Δ1 ++ Π ++ Δ2)
     ≡ ⟦ τ ⟧ (Δ1 ++ Δ2).
   Proof.
-    revert Δ1 Π Δ2. induction τ=> Δ1 Π Δ2; simpl; auto.
-    - intros w; simpl; properness; auto;
-        match goal with IH : ∀ _, _ |- _ => by apply IH end.
-    - intros w; simpl; properness; auto;
-        match goal with IH : ∀ _, _ |- _ => by apply IH end.
-    - intros w; simpl; properness; auto;
-        match goal with IH : ∀ _, _ |- _ => by apply IH end.
-    - apply fixpoint_proper=> τi w /=.
-      properness; auto.
-      match goal with IH : ∀ _, _ |- _ => by apply (IH (_ :: _)) end.
+    revert Δ1 Π Δ2. induction τ=> Δ1 Π Δ2; simpl; auto; intros ?; simpl.
+    - by repeat (f_equiv; try match goal with IH : ∀ _, _ |- _ => by apply IH end).
+    - by repeat (f_equiv; try match goal with IH : ∀ _, _ |- _ => by apply IH end).
+    - by repeat (f_equiv; try match goal with IH : ∀ _, _ |- _ => by apply IH end).
+    - f_equiv.
+      apply fixpoint_proper=> τi w /=.
+      by repeat (f_equiv; try match goal with IH : ∀ _, _ |- _ => by apply (IH (_ :: _)) end).
     - rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl.
       { by rewrite !lookup_app_l. }
-      intros ?; simpl.
       rewrite !lookup_app_r; [|lia ..]; do 3 f_equiv; lia.
-    - intros w; simpl; properness; auto.
-      match goal with IH : ∀ _, _ |- _ => by apply (IH (_ :: _)) end.
-    - intros w; simpl; properness; auto.
-      match goal with IH : ∀ _, _ |- _ => by apply (IH (_ :: _)) end.
-    - intros w; simpl; properness; auto.
-      match goal with IH : ∀ _, _ |- _ => by apply IH end.
+    - by repeat (f_equiv; try match goal with IH : ∀ _, _ |- _ => by apply (IH (_ :: _)) end).
+    - by repeat (f_equiv; try match goal with IH : ∀ _, _ |- _ => by apply (IH (_ :: _)) end).
+    - by repeat (f_equiv; try match goal with IH : ∀ _, _ |- _ => by apply IH end).
   Qed.
 
   Lemma interp_subst_up Δ1 Δ2 τ τ' :
     ⟦ τ ⟧ (Δ1 ++ interp τ' Δ2 :: Δ2)
     ≡ ⟦ τ.[upn (length Δ1) (τ' .: ids)] ⟧ (Δ1 ++ Δ2).
   Proof.
-    revert Δ1 Δ2; induction τ=> Δ1 Δ2; simpl; auto.
-    - intros w; simpl; properness; auto;
-        match goal with IH : ∀ _, _ |- _ => by apply IH end.
-    - intros w; simpl; properness; auto;
-        match goal with IH : ∀ _, _ |- _ => by apply IH end.
-    - intros w; simpl; properness; auto;
-        match goal with IH : ∀ _, _ |- _ => by apply IH end.
-    - apply fixpoint_proper=> τi w /=.
-      properness; auto.
-      match goal with IH : ∀ _, _ |- _ => by apply (IH (_ :: _)) end.
+    revert Δ1 Δ2; induction τ=> Δ1 Δ2; simpl; auto; intros ?; simpl.
+    - by repeat (f_equiv; try match goal with IH : ∀ _, _ |- _ => by apply IH end).
+    - by repeat (f_equiv; try match goal with IH : ∀ _, _ |- _ => by apply IH end).
+    - by repeat (f_equiv; try match goal with IH : ∀ _, _ |- _ => by apply IH end).
+    - f_equiv.
+      apply fixpoint_proper=> τi w /=.
+      by repeat (f_equiv; try match goal with IH : ∀ _, _ |- _ => by apply (IH (_ :: _)) end).
     - match goal with |- context [_ !! ?x] => rename x into idx end.
       rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl.
       { by rewrite !lookup_app_l. }
-      intros ?; simpl.
       rewrite !lookup_app_r; [|lia ..].
       case EQ: (idx - length Δ1) => [|n]; simpl.
       { symmetry. asimpl. apply (interp_weaken [] Δ1 Δ2 τ'). }
       rewrite !lookup_app_r; [|lia ..]. do 3 f_equiv. lia.
-    - intros w; simpl; properness; auto.
-      match goal with IH : ∀ _, _ |- _ => by apply (IH (_ :: _)) end.
-    - intros w; simpl; properness; auto.
-      match goal with IH : ∀ _, _ |- _ => by apply (IH (_ :: _)) end.
-    - intros w; simpl; properness; auto.
-      match goal with IH : ∀ _, _ |- _ => by apply IH end.
+    - by repeat (f_equiv; try match goal with IH : ∀ _, _ |- _ => by apply (IH (_ :: _)) end).
+    - by repeat (f_equiv; try match goal with IH : ∀ _, _ |- _ => by apply (IH (_ :: _)) end).
+    - by repeat (f_equiv; try match goal with IH : ∀ _, _ |- _ => by apply IH end).
   Qed.
 
   Lemma interp_subst Δ2 τ τ' v : ⟦ τ ⟧ (⟦ τ' ⟧ Δ2 :: Δ2) v ≡ ⟦ τ.[τ'/] ⟧ Δ2 v.
diff --git a/theories/logrel/stlc/fundamental.v b/theories/logrel/stlc/fundamental.v
index 613cfe4b674a1ebd80aa97101ebfdaf65e29366a..028e2722db05d6311cebf1f47a0b0b1849059d65 100644
--- a/theories/logrel/stlc/fundamental.v
+++ b/theories/logrel/stlc/fundamental.v
@@ -15,10 +15,9 @@ Section typed_interp.
   specific [state_interp], but STLC has no state so it does not care. *)
   Context `{irisGS stlc_lang Σ}.
 
-  Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) constr(Hv) constr(Hp) :=
-    iApply (wp_bind (fill [ctx]));
-    iApply (wp_wand with "[-]"); [iApply Hp; trivial|]; cbn;
-    iIntros (v) Hv.
+  Lemma interp_expr_bind K e τ τ' :
+    ⟦ τ ⟧ₑ e -∗ (∀ v, ⟦ τ ⟧ v -∗ ⟦ τ' ⟧ₑ (fill K (#v))) -∗ ⟦ τ' ⟧ₑ (fill K e).
+  Proof. iIntros; iApply wp_bind; iApply (wp_wand with "[$]"); done. Qed.
 
   Theorem fundamental Γ e τ : Γ ⊢ₜ e : τ → ⊢ Γ ⊨ e : τ.
   Proof.
@@ -30,24 +29,33 @@ Section typed_interp.
       by iApply wp_value.
     - (* unit *) by iApply wp_value.
     - (* pair *)
-      smart_wp_bind (PairLCtx _.[env_subst vs]) v "# Hv" "IH".
-      smart_wp_bind (PairRCtx v) v' "# Hv'" "IH1".
-      iApply wp_value; eauto 10.
+      iApply (interp_expr_bind [PairLCtx _]); first by iApply "IH".
+      iIntros (v) "#Hv /=".
+      iApply (interp_expr_bind [PairRCtx _]); first by iApply "IH1".
+      iIntros (w) "#Hw /=".
+      iApply wp_value; simpl; eauto 10.
     - (* fst *)
-      smart_wp_bind (FstCtx) v "# Hv" "IH"; cbn.
+      iApply (interp_expr_bind [FstCtx]); first by iApply "IH".
+      iIntros (v) "#Hv /=".
       iDestruct "Hv" as (w1 w2) "#[-> [H2 H3]] /=".
       iApply wp_pure_step_later; auto. iIntros "!> _". by iApply wp_value.
     - (* snd *)
-      smart_wp_bind (SndCtx) v "# Hv" "IH"; cbn.
+      iApply (interp_expr_bind [SndCtx]); first by iApply "IH".
+      iIntros (v) "#Hv /=".
       iDestruct "Hv" as (w1 w2) "#[-> [H2 H3]] /=".
       iApply wp_pure_step_later; auto. iIntros "!> _". by iApply wp_value.
     - (* injl *)
-      smart_wp_bind (InjLCtx) v "# Hv" "IH". by iApply wp_value; eauto.
+      iApply (interp_expr_bind [InjLCtx]); first by iApply "IH".
+      iIntros (v) "#Hv /=".
+      iApply wp_value; simpl; eauto.
     - (* injr *)
-      smart_wp_bind (InjRCtx) v "# Hv" "IH". by iApply wp_value; eauto.
+      iApply (interp_expr_bind [InjRCtx]); first by iApply "IH".
+      iIntros (v) "#Hv /=".
+      iApply wp_value; simpl; eauto.
     - (* case *)
       iDestruct (interp_env_length with "[]") as %Hlen; auto.
-      smart_wp_bind (CaseCtx _ _) v "# Hv" "IH"; cbn.
+      iApply (interp_expr_bind [CaseCtx _ _]); first by iApply "IH".
+      iIntros (v) "#Hv /=".
       iDestruct "Hv" as "[Hv|Hv]"; iDestruct "Hv" as (w) "[-> Hw] /=".
       + simpl. iApply wp_pure_step_later; auto. asimpl.
         iIntros "!> _". iApply ("IH1" $! (w::vs)).
@@ -61,8 +69,11 @@ Section typed_interp.
       iApply wp_pure_step_later; auto. iIntros "!> _". asimpl.
       iApply ("IH" $! (w :: vs)). iApply interp_env_cons; by iSplit.
     - (* app *)
-      smart_wp_bind (AppLCtx (_.[env_subst vs])) v "#Hv" "IH".
-      smart_wp_bind (AppRCtx v) w "#Hw" "IH1".
+      iApply (interp_expr_bind [AppLCtx _]); first by iApply "IH".
+      simpl.
+      iIntros (v) "#Hv /=".
+      iApply (interp_expr_bind [AppRCtx _]); first by iApply "IH1".
+      iIntros (w) "#Hw/=".
       iApply "Hv"; auto.
   Qed.
 End typed_interp.