diff --git a/opam b/opam
index b9df35c3554f24f219c67dddeb31951f3106412f..2a1f61e764f81ee07c48f77558d93d4971f8094d 100644
--- a/opam
+++ b/opam
@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/actris" ]
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2021-01-25.1.21b7ffa1") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2021-01-26.0.a26cf167") | (= "dev") }
 ]
diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index 5def6354b8f8d084315652ac252db5dbcb45e01d..99e90d5d06734834c4c32b829978aa622ea24322 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -205,10 +205,10 @@ Section channel.
     {{{ c1 c2, RET (c1,c2); c1 ↣ p ∗ c2 ↣ iProto_dual p }}}.
   Proof.
     iIntros (Φ _) "HΦ". wp_lam.
-    wp_apply (lnil_spec internal_eq with "[//]"); iIntros (l) "Hl".
-    wp_apply (lnil_spec internal_eq with "[//]"); iIntros (r) "Hr".
+    wp_smart_apply (lnil_spec internal_eq with "[//]"); iIntros (l) "Hl".
+    wp_smart_apply (lnil_spec internal_eq with "[//]"); iIntros (r) "Hr".
     iMod (iProto_init p) as (γp) "(Hctx & Hcl & Hcr)".
-    wp_apply (newlock_spec (∃ vsl vsr,
+    wp_smart_apply (newlock_spec (∃ vsl vsr,
       llist internal_eq l vsl ∗ llist internal_eq r vsr ∗
       iProto_ctx γp vsl vsr) with "[Hl Hr Hctx]").
     { iExists [], []. iFrame. }
@@ -224,9 +224,9 @@ Section channel.
     WP start_chan f {{ Φ }}.
   Proof.
     iIntros "Hfork HΦ". wp_lam.
-    wp_apply (new_chan_spec p with "[//]"); iIntros (c1 c2) "[Hc1 Hc2]".
-    wp_apply (wp_fork with "[Hfork Hc2]").
-    { iNext. wp_apply ("Hfork" with "Hc2"). }
+    wp_smart_apply (new_chan_spec p with "[//]"); iIntros (c1 c2) "[Hc1 Hc2]".
+    wp_smart_apply (wp_fork with "[Hfork Hc2]").
+    { iNext. wp_smart_apply ("Hfork" with "Hc2"). }
     wp_pures. iApply ("HΦ" with "Hc1").
   Qed.
 
@@ -237,21 +237,21 @@ Section channel.
   Proof.
     rewrite iProto_mapsto_eq. iIntros (Φ) "Hc HΦ". wp_lam; wp_pures.
     iDestruct "Hc" as (γ s l r lk ->) "[#Hlk H]"; wp_pures.
-    wp_apply (acquire_spec with "Hlk"); iIntros "[Hlkd Hinv]".
+    wp_smart_apply (acquire_spec with "Hlk"); iIntros "[Hlkd Hinv]".
     iDestruct "Hinv" as (vsl vsr) "(Hl & Hr & Hctx)". destruct s; simpl.
     - iMod (iProto_send_l with "Hctx H []") as "[Hctx H]".
       { rewrite iMsg_base_eq /=; auto. }
-      wp_apply (lsnoc_spec with "[$Hl //]"); iIntros "Hl".
-      wp_apply (llength_spec with "[$Hr //]"); iIntros "Hr".
-      wp_apply skipN_spec.
-      wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
+      wp_smart_apply (lsnoc_spec with "[$Hl //]"); iIntros "Hl".
+      wp_smart_apply (llength_spec with "[$Hr //]"); iIntros "Hr".
+      wp_smart_apply skipN_spec.
+      wp_smart_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
       iIntros "_". iApply "HΦ". iExists γ, Left, l, r, lk. eauto 10 with iFrame.
     - iMod (iProto_send_r with "Hctx H []") as "[Hctx H]".
       { rewrite iMsg_base_eq /=; auto. }
-      wp_apply (lsnoc_spec with "[$Hr //]"); iIntros "Hr".
-      wp_apply (llength_spec with "[$Hl //]"); iIntros "Hl".
-      wp_apply skipN_spec.
-      wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
+      wp_smart_apply (lsnoc_spec with "[$Hr //]"); iIntros "Hr".
+      wp_smart_apply (llength_spec with "[$Hl //]"); iIntros "Hl".
+      wp_smart_apply skipN_spec.
+      wp_smart_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
       iIntros "_". iApply "HΦ". iExists γ, Right, l, r, lk. eauto 10 with iFrame.
   Qed.
 
@@ -279,31 +279,31 @@ Section channel.
   Proof.
     rewrite iProto_mapsto_eq. iIntros (Φ) "Hc HΦ". wp_lam; wp_pures.
     iDestruct "Hc" as (γ s l r lk ->) "[#Hlk H]"; wp_pures.
-    wp_apply (acquire_spec with "Hlk"); iIntros "[Hlkd Hinv]".
+    wp_smart_apply (acquire_spec with "Hlk"); iIntros "[Hlkd Hinv]".
     iDestruct "Hinv" as (vsl vsr) "(Hl & Hr & Hctx)". destruct s; simpl.
-    - wp_apply (lisnil_spec with "Hr"); iIntros "Hr".
+    - wp_smart_apply (lisnil_spec with "Hr"); iIntros "Hr".
       destruct vsr as [|vr vsr]; wp_pures.
-      { wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
+      { wp_smart_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
         iIntros "_". wp_pures. iModIntro. iApply "HΦ". iLeft. iSplit; [done|].
         iExists γ, Left, l, r, lk. eauto 10 with iFrame. }
-      wp_apply (lpop_spec with "Hr"); iIntros (v') "[% Hr]"; simplify_eq/=.
+      wp_smart_apply (lpop_spec with "Hr"); iIntros (v') "[% Hr]"; simplify_eq/=.
       iMod (iProto_recv_l with "Hctx H") as (q) "(Hctx & H & Hm)". wp_pures.
       rewrite iMsg_base_eq.
       iDestruct (iMsg_texist_exist with "Hm") as (x <-) "[Hp HP]".
-      wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
+      wp_smart_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
       iIntros "_". wp_pures. iModIntro. iApply "HΦ". iRight. iExists x. iSplit; [done|].
       iFrame "HP". iExists γ, Left, l, r, lk. iSplit; [done|]. iFrame "Hlk".
       by iRewrite "Hp".
-    - wp_apply (lisnil_spec with "Hl"); iIntros "Hl".
+    - wp_smart_apply (lisnil_spec with "Hl"); iIntros "Hl".
       destruct vsl as [|vl vsl]; wp_pures.
-      { wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
+      { wp_smart_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
         iIntros "_". wp_pures. iModIntro. iApply "HΦ". iLeft. iSplit; [done|].
         iExists γ, Right, l, r, lk. eauto 10 with iFrame. }
-      wp_apply (lpop_spec with "Hl"); iIntros (v') "[% Hl]"; simplify_eq/=.
+      wp_smart_apply (lpop_spec with "Hl"); iIntros (v') "[% Hl]"; simplify_eq/=.
       iMod (iProto_recv_r with "Hctx H") as (q) "(Hctx & H & Hm)". wp_pures.
       rewrite iMsg_base_eq.
       iDestruct (iMsg_texist_exist with "Hm") as (x <-) "[Hp HP]".
-      wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
+      wp_smart_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
       iIntros "_". wp_pures. iModIntro. iApply "HΦ". iRight. iExists x. iSplit; [done|].
       iFrame "HP". iExists γ, Right, l, r, lk. iSplit; [done|]. iFrame "Hlk".
       by iRewrite "Hp".
@@ -315,7 +315,7 @@ Section channel.
     {{{ x, RET v x; c ↣ p x ∗ P x }}}.
   Proof.
     iIntros (Φ) "Hc HΦ". iLöb as "IH". wp_lam.
-    wp_apply (try_recv_spec with "Hc"); iIntros (w) "[[-> H]|H]".
+    wp_smart_apply (try_recv_spec with "Hc"); iIntros (w) "[[-> H]|H]".
     { wp_pures. by iApply ("IH" with "[$]"). }
     iDestruct "H" as (x ->) "[Hc HP]". wp_pures. iApply "HΦ". by iFrame.
   Qed.
diff --git a/theories/examples/basics.v b/theories/examples/basics.v
index e984619349a26f2d3a0423b246e5574c581dd475..bee5f69a2b6912eb0370f66fe5fdab07d31b2aee 100644
--- a/theories/examples/basics.v
+++ b/theories/examples/basics.v
@@ -207,7 +207,7 @@ Definition prot_swap_loop : iProto Σ :=
 Lemma prog_spec : {{{ True }}} prog #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_apply (start_chan_spec prot); iIntros (c) "Hc".
+  wp_smart_apply (start_chan_spec prot); iIntros (c) "Hc".
   - by wp_send with "[]".
   - wp_recv as "_". by iApply "HΦ".
 Qed.
@@ -215,7 +215,7 @@ Qed.
 Lemma prog_ref_spec : {{{ True }}} prog_ref #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_apply (start_chan_spec prot_ref); iIntros (c) "Hc".
+  wp_smart_apply (start_chan_spec prot_ref); iIntros (c) "Hc".
   - wp_alloc l as "Hl". by wp_send with "[$Hl]".
   - wp_recv (l) as "Hl". wp_load. by iApply "HΦ".
 Qed.
@@ -223,8 +223,8 @@ Qed.
 Lemma prog_del_spec : {{{ True }}} prog_del #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_apply (start_chan_spec prot_del); iIntros (c) "Hc".
-  - wp_apply (new_chan_spec prot with "[//]").
+  wp_smart_apply (start_chan_spec prot_del); iIntros (c) "Hc".
+  - wp_smart_apply (new_chan_spec prot with "[//]").
     iIntros (c2 c2') "[Hc2 Hc2']". wp_send with "[$Hc2]". by wp_send with "[]".
   - wp_recv (c2) as "Hc2". wp_recv as "_". by iApply "HΦ".
 Qed.
@@ -232,7 +232,7 @@ Qed.
 Lemma prog_dep_spec : {{{ True }}} prog_dep #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_apply (start_chan_spec prot_dep); iIntros (c) "Hc".
+  wp_smart_apply (start_chan_spec prot_dep); iIntros (c) "Hc".
   - wp_recv (x) as "_". by wp_send with "[]".
   - wp_send with "[//]". wp_recv as "_". by iApply "HΦ".
 Qed.
@@ -240,7 +240,7 @@ Qed.
 Lemma prog2_ref_spec : {{{ True }}} prog_dep_ref #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_apply (start_chan_spec prot_dep_ref); iIntros (c) "Hc".
+  wp_smart_apply (start_chan_spec prot_dep_ref); iIntros (c) "Hc".
   - wp_recv (l x) as "Hl". wp_load. wp_store. by wp_send with "[Hl]".
   - wp_alloc l as "Hl". wp_send with "[$Hl]". wp_recv as "Hl". wp_load.
     by iApply "HΦ".
@@ -249,8 +249,8 @@ Qed.
 Lemma prog_dep_del_spec : {{{ True }}} prog_dep_del #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_apply (start_chan_spec prot_dep_del); iIntros (c) "Hc".
-  - wp_apply (new_chan_spec prot_dep with "[//]"); iIntros (c2 c2') "[Hc2 Hc2']".
+  wp_smart_apply (start_chan_spec prot_dep_del); iIntros (c) "Hc".
+  - wp_smart_apply (new_chan_spec prot_dep with "[//]"); iIntros (c2 c2') "[Hc2 Hc2']".
     wp_send with "[$Hc2]". wp_recv (x) as "_". by wp_send with "[]".
   - wp_recv (c2) as "Hc2". wp_send with "[//]". wp_recv as "_".
     by iApply "HΦ".
@@ -259,9 +259,9 @@ Qed.
 Lemma prog_dep_del_2_spec : {{{ True }}} prog_dep_del_2 #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_apply (start_chan_spec prot_dep_del_2); iIntros (c) "Hc".
+  wp_smart_apply (start_chan_spec prot_dep_del_2); iIntros (c) "Hc".
   { wp_recv (c2) as "Hc2". wp_send with "[//]". by wp_send with "[$Hc2]". }
-  wp_apply (start_chan_spec prot_dep); iIntros (c2) "Hc2".
+  wp_smart_apply (start_chan_spec prot_dep); iIntros (c2) "Hc2".
   { wp_recv (x) as "_". by wp_send with "[//]". }
   wp_send with "[$Hc2]". wp_recv as "Hc2". wp_recv as "_". by iApply "HΦ".
 Qed.
@@ -269,10 +269,10 @@ Qed.
 Lemma prog_dep_del_3_spec : {{{ True }}} prog_dep_del_3 #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_apply (start_chan_spec prot_dep_del_3); iIntros (c) "Hc".
+  wp_smart_apply (start_chan_spec prot_dep_del_3); iIntros (c) "Hc".
   { wp_recv (c2) as "Hc2". wp_recv (y) as "_".
     wp_send with "[//]". by wp_send with "[$Hc2]". }
-  wp_apply (start_chan_spec prot_dep); iIntros (c2) "Hc2".
+  wp_smart_apply (start_chan_spec prot_dep); iIntros (c2) "Hc2".
   { wp_recv (x) as "_". by wp_send with "[//]". }
   wp_send with "[$Hc2]". wp_send with "[//]".
   wp_recv as "Hc2". wp_recv as "_". by iApply "HΦ".
@@ -281,7 +281,7 @@ Qed.
 Lemma prog_loop_spec : {{{ True }}} prog_loop #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_apply (start_chan_spec prot_loop); iIntros (c) "Hc".
+  wp_smart_apply (start_chan_spec prot_loop); iIntros (c) "Hc".
   - iLöb as "IH".
     wp_recv (x) as "_". wp_send with "[//]".
     do 2 wp_pure _. by iApply "IH".
@@ -292,14 +292,14 @@ Qed.
 Lemma prog_fun_spec : {{{ True }}} prog_fun #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_apply (start_chan_spec prot_fun); iIntros (c) "Hc".
+  wp_smart_apply (start_chan_spec prot_fun); iIntros (c) "Hc".
   - wp_recv (P Ψ vf) as "#Hf". wp_send with "[]"; last done.
-    iIntros "!>" (Ψ') "HP HΨ'". wp_apply ("Hf" with "HP"); iIntros (x) "HΨ".
+    iIntros "!>" (Ψ') "HP HΨ'". wp_smart_apply ("Hf" with "HP"); iIntros (x) "HΨ".
     wp_pures. by iApply "HΨ'".
   - wp_alloc l as "Hl".
     wp_send ((l ↦ #40)%I (λ w, ⌜ w = 40%Z ⌝ ∗ l ↦ #40)%I) with "[]".
     { iIntros "!>" (Ψ') "Hl HΨ'". wp_load. iApply "HΨ'"; auto. }
-    wp_recv (vg) as "#Hg". wp_apply ("Hg" with "Hl"); iIntros (x) "[-> Hl]".
+    wp_recv (vg) as "#Hg". wp_smart_apply ("Hg" with "Hl"); iIntros (x) "[-> Hl]".
     by iApply "HΦ".
 Qed.
 
@@ -307,33 +307,33 @@ Lemma prog_lock_spec `{!lockG Σ, contributionG Σ unitUR} :
   {{{ True }}} prog_lock #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_apply (start_chan_spec (prot_lock 2)); iIntros (c) "Hc".
+  wp_smart_apply (start_chan_spec (prot_lock 2)); iIntros (c) "Hc".
   - iMod contribution_init as (γ) "Hs".
     iMod (alloc_client with "Hs") as "[Hs Hcl1]".
     iMod (alloc_client with "Hs") as "[Hs Hcl2]".
-    wp_apply (newlock_spec (∃ n, server γ n ε ∗
+    wp_smart_apply (newlock_spec (∃ n, server γ n ε ∗
       c ↣ iProto_dual (prot_lock n))%I
       with "[Hc Hs]"); first by eauto with iFrame.
     iIntros (lk γlk) "#Hlk".
     iAssert (client γ ε -∗
       WP acquire lk;; send c #21;; release lk {{ _, True }})%I with "[]" as "#Hhelp".
     { iIntros "Hcl".
-      wp_apply (acquire_spec with "[$]"); iIntros "[Hl H]".
+      wp_smart_apply (acquire_spec with "[$]"); iIntros "[Hl H]".
       iDestruct "H" as (n) "[Hs Hc]".
       iDestruct (server_agree with "Hs Hcl") as %[? _].
       destruct n as [|n]=> //=. wp_send with "[//]".
       iMod (dealloc_client with "Hs Hcl") as "Hs /=".
-      wp_apply (release_spec with "[$Hlk $Hl Hc Hs]"); eauto with iFrame. }
-    wp_apply (wp_fork with "[Hcl1]").
+      wp_smart_apply (release_spec with "[$Hlk $Hl Hc Hs]"); eauto with iFrame. }
+    wp_smart_apply (wp_fork with "[Hcl1]").
     { iNext. by iApply "Hhelp". }
-    by wp_apply "Hhelp".
+    by wp_smart_apply "Hhelp".
   - wp_recv as "_". wp_recv as "_". wp_pures. by iApply "HΦ".
 Qed.
 
 Lemma prog_swap_spec : {{{ True }}} prog_swap #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_apply (start_chan_spec prot_swap); iIntros (c) "Hc".
+  wp_smart_apply (start_chan_spec prot_swap); iIntros (c) "Hc".
   - wp_send with "[//]". wp_recv (x) as "_". by wp_send with "[//]".
   - wp_send with "[//]". wp_recv as "_". wp_recv as "_".
     wp_pures. by iApply "HΦ".
@@ -342,7 +342,7 @@ Qed.
 Lemma prog_swap_twice_spec : {{{ True }}} prog_swap_twice #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_apply (start_chan_spec prot_swap_twice); iIntros (c) "Hc".
+  wp_smart_apply (start_chan_spec prot_swap_twice); iIntros (c) "Hc".
   - wp_send with "[//]". wp_recv (x1) as "_". wp_recv (x2) as "_".
     by wp_send with "[//]".
   - wp_send with "[//]". wp_send with "[//]". wp_recv as "_". wp_recv as "_".
@@ -352,7 +352,7 @@ Qed.
 Lemma prog_swap_loop_spec : {{{ True }}} prog_swap_loop #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_apply (start_chan_spec prot_loop); iIntros (c) "Hc".
+  wp_smart_apply (start_chan_spec prot_loop); iIntros (c) "Hc".
   - iLöb as "IH".
     wp_recv (x) as "_". wp_send with "[//]".
     do 2 wp_pure _. by iApply "IH".
@@ -366,7 +366,7 @@ Actris journal paper *)
 Lemma prog_ref_swap_loop_spec : ∀ Φ, Φ #42 -∗ WP prog_ref_swap_loop #() {{ Φ }}.
 Proof.
   iIntros (Φ) "HΦ". wp_lam.
-  wp_apply (start_chan_spec prot_ref_loop); iIntros (c) "Hc".
+  wp_smart_apply (start_chan_spec prot_ref_loop); iIntros (c) "Hc".
   - iLöb as "IH". wp_lam.
     wp_recv (l x) as "Hl". wp_load. wp_store. wp_send with "[$Hl]".
     do 2 wp_pure _. by iApply "IH".
diff --git a/theories/examples/list_rev.v b/theories/examples/list_rev.v
index e499654ed6805a5d762ece2ca70063140b5b3125..a851ea08b64a17ab7c3fde4288620dc0c3fc96f2 100644
--- a/theories/examples/list_rev.v
+++ b/theories/examples/list_rev.v
@@ -25,7 +25,7 @@ Section list_rev_example.
     {{{ RET #(); c ↣ prot }}}.
   Proof.
     iIntros (Φ) "Hc HΦ".
-    wp_lam. wp_recv (l vs) as "Hl". wp_apply (lreverse_spec with "Hl").
+    wp_lam. wp_recv (l vs) as "Hl". wp_smart_apply (lreverse_spec with "Hl").
     iIntros "Hl". wp_send with "[$Hl]". iApply ("HΦ" with "Hc").
   Qed.
 
@@ -75,7 +75,7 @@ Section list_rev_example.
     {{{ RET #(); llist IT l (reverse xs) }}}.
   Proof.
     iIntros (Φ) "Hl HΦ". wp_lam.
-    wp_apply (start_chan_spec (list_rev_prot)%proto); iIntros (c) "Hc".
+    wp_smart_apply (start_chan_spec (list_rev_prot)%proto); iIntros (c) "Hc".
     - rewrite -(iProto_app_end_r list_rev_prot).
       iApply (list_rev_service_spec with "Hc"). eauto.
     - iDestruct (iProto_mapsto_le _ _ (list_rev_protI IT) with "Hc []") as "Hc".
diff --git a/theories/examples/map_reduce.v b/theories/examples/map_reduce.v
index 466eaedb6892b3d4d2844179148bd923770a5296..a58480332962933c1cccfcd139da3003f23015fe 100644
--- a/theories/examples/map_reduce.v
+++ b/theories/examples/map_reduce.v
@@ -143,20 +143,20 @@ Section mapper.
     { destruct Hn as [-> ->]; first lia.
       iApply ("HΦ" $! []). rewrite right_id_L. auto with iFrame. }
     destruct n as [|n]=> //=. wp_branch as %?|%_; wp_pures.
-    - wp_apply (lisnil_spec with "Hl"); iIntros "Hl".
+    - wp_smart_apply (lisnil_spec with "Hl"); iIntros "Hl".
       destruct xs as [|x xs]; csimpl; wp_pures.
       + wp_select. wp_pures. rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
         iApply ("IH" $! _ [] with "[%] Hl Hcmap Hcsort HΦ"); naive_solver.
-      + wp_select. wp_apply (lpop_spec with "Hl"); iIntros (v) "[HIx Hl]".
+      + wp_select. wp_smart_apply (lpop_spec with "Hl"); iIntros (v) "[HIx Hl]".
         wp_send with "[$HIx]".
-        wp_apply ("IH" with "[%] Hl Hcmap Hcsort"); first done. iIntros (ys').
+        wp_smart_apply ("IH" with "[%] Hl Hcmap Hcsort"); first done. iIntros (ys').
         rewrite gmultiset_elements_disj_union gmultiset_elements_singleton.
         rewrite assoc_L -(comm _ [x]). iApply "HΦ".
     - wp_recv (x k) as (Hx) "Hk".
       rewrite -(right_id END%proto _ (sort_fg_head_protocol _ _ _)).
-      wp_apply (send_all_spec with "[$Hk $Hcsort]"); iIntros "[_ Hcsort]".
+      wp_smart_apply (send_all_spec with "[$Hk $Hcsort]"); iIntros "[_ Hcsort]".
       rewrite right_id.
-      wp_apply ("IH" with "[] Hl Hcmap Hcsort"); first done.
+      wp_smart_apply ("IH" with "[] Hl Hcmap Hcsort"); first done.
       iIntros (ys'). iDestruct 1 as (Hys) "Hcsort"; simplify_eq/=.
       rewrite -assoc_L. iApply ("HΦ" $! (map x ++ ys') with "[$Hcsort]").
       iPureIntro. rewrite (gmultiset_disj_union_difference {[ x ]} X)
@@ -193,8 +193,8 @@ Section mapper.
      iEval (rewrite !right_id_L); auto with iFrame. }
     wp_recv ([j y] ?) as (Htl w ->) "HIy /=". wp_pures. rewrite -assoc_L.
     case_bool_decide as Hij; simplify_eq/=; wp_pures.
-    - wp_apply (lcons_spec with "[$Hl $HIy]"); iIntros "Hl".
-      rewrite -reverse_snoc. wp_apply ("IH" $! (ys ++ [y])
+    - wp_smart_apply (lcons_spec with "[$Hl $HIy]"); iIntros "Hl".
+      rewrite -reverse_snoc. wp_smart_apply ("IH" $! (ys ++ [y])
         with "[%] [%] [//] Hl [Hcsort] [HΦ]"); try iClear "IH".
       + intros ?; discriminate_list.
       + rewrite fmap_app /= assoc_L. by apply Sorted_snoc.
@@ -244,9 +244,9 @@ Section mapper.
       + wp_select. wp_pures. rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
         iApply ("IH" $! _ _ None
           with "[%] [%] [%] Hl Hcsort Hcred [] HΦ"); naive_solver.
-      + wp_apply (lnil_spec (IB i) with "[//]"); iIntros (k) "Hk".
-        wp_apply (lcons_spec with "[$Hk $HImiy]"); iIntros "Hk".
-        wp_apply (par_map_reduce_collect_spec _ _ _ _ _ [_] 
+      + wp_smart_apply (lnil_spec (IB i) with "[//]"); iIntros (k) "Hk".
+        wp_smart_apply (lcons_spec with "[$Hk $HImiy]"); iIntros "Hk".
+        wp_smart_apply (par_map_reduce_collect_spec _ _ _ _ _ [_] 
           with "[$Hk $Hcsort]"); try done.
         iIntros (ys' miy). iDestruct 1 as (? Hmiy') "(Hk & Hcsort & HImiy)"; csimpl.
         wp_select; wp_pures. wp_send ((i, reverse (y :: ys'))) with "[Hk]".
@@ -261,8 +261,8 @@ Section mapper.
         rewrite !bind_app /= right_id_L -!assoc_L -(comm _ zs') !assoc_L.
         apply (inj (.++ _)).
     - wp_recv ([i ys] k) as (Hy) "Hk".
-      wp_apply (lprep_spec with "[$Hl $Hk]"); iIntros "[Hl _]".
-      wp_apply ("IH" with "[ ] [//] [//] Hl Hcsort Hcred HImiy"); first done.
+      wp_smart_apply (lprep_spec with "[$Hl $Hk]"); iIntros "[Hl _]".
+      wp_smart_apply ("IH" with "[ ] [//] [//] Hl Hcsort Hcred HImiy"); first done.
       iIntros (zs'); iDestruct 1 as (Hzs) "HIC"; simplify_eq/=.
       iApply ("HΦ" $! (zs' ++ red i ys)). iSplit; last by rewrite -assoc_L.
       iPureIntro. rewrite (gmultiset_disj_union_difference {[ i,ys ]} Y)
@@ -281,25 +281,25 @@ Section mapper.
     {{{ zs, RET #(); ⌜zs ≡ₚ map_reduce map red xs⌝ ∗ llist IC l zs }}}.
   Proof.
     iIntros (??) "#Hmap #Hred !>"; iIntros (Φ) "Hl HΦ". wp_lam; wp_pures.
-    wp_apply (start_chan_spec (par_map_protocol IA IZB map n ∅));
+    wp_smart_apply (start_chan_spec (par_map_protocol IA IZB map n ∅));
       iIntros (cmap) "// Hcmap".
-    { wp_pures. wp_apply (par_map_service_spec with "Hmap Hcmap"); auto. }
-    wp_apply (start_chan_spec (sort_fg_protocol IZB RZB <++> END)%proto);
+    { wp_pures. wp_smart_apply (par_map_service_spec with "Hmap Hcmap"); auto. }
+    wp_smart_apply (start_chan_spec (sort_fg_protocol IZB RZB <++> END)%proto);
       iIntros (csort) "Hcsort".
-    { wp_apply (sort_service_fg_spec with "[] Hcsort"); last by auto.
+    { wp_smart_apply (sort_service_fg_spec with "[] Hcsort"); last by auto.
       iApply RZB_cmp_spec. }
     rewrite right_id.
-    wp_apply (par_map_reduce_map_spec with "[$Hl $Hcmap $Hcsort]"); first lia.
+    wp_smart_apply (par_map_reduce_map_spec with "[$Hl $Hcmap $Hcsort]"); first lia.
     iIntros (iys). rewrite gmultiset_elements_empty right_id_L.
     iDestruct 1 as (Hiys) "[Hl Hcsort] /=". wp_select; wp_pures; simpl.
-    wp_apply (start_chan_spec (par_map_protocol IZBs IC (curry red) m ∅));
+    wp_smart_apply (start_chan_spec (par_map_protocol IZBs IC (curry red) m ∅));
       iIntros (cred) "// Hcred".
-    { wp_pures. wp_apply (par_map_service_spec with "Hred Hcred"); auto. }
+    { wp_pures. wp_smart_apply (par_map_service_spec with "Hred Hcred"); auto. }
     wp_branch as %_|%Hnil; last first.
     { wp_pures. iApply ("HΦ" $! [] with "[$Hl]"); simpl.
       by rewrite /map_reduce /= -Hiys -Hnil. }
     wp_recv ([i y] ?) as (_ w ->) "HIB /="; wp_pures.
-    wp_apply (par_map_reduce_reduce_spec _ _ [] (Some (i, y, w)) []
+    wp_smart_apply (par_map_reduce_reduce_spec _ _ [] (Some (i, y, w)) []
       with "[$Hl $Hcsort $Hcred $HIB]"); simpl; auto; [lia|set_solver|].
     iIntros (zs). rewrite /= gmultiset_elements_empty !right_id.
     iDestruct 1 as (Hzs) "Hk".
diff --git a/theories/examples/par_map.v b/theories/examples/par_map.v
index 638efb9ba66e4b0ae7dc3b1e37b7dafdab27783a..bcc24fbefa560f6a2e7346649e98032487ad3866 100644
--- a/theories/examples/par_map.v
+++ b/theories/examples/par_map.v
@@ -96,7 +96,7 @@ Section map.
   Proof.
     iIntros "#Hmap !>" (Φ) "[#Hlk Hγ] HΦ". iLöb as "IH".
     wp_rec; wp_pures.
-    wp_apply (acquire_spec with "Hlk"); iIntros "[Hl H]".
+    wp_smart_apply (acquire_spec with "Hlk"); iIntros "[Hl H]".
     iDestruct "H" as (i X) "[Hs Hc]".
     iDestruct (@server_agree with "Hs Hγ") as %[??]; destruct i as [|i]=>//=.
     iAssert ⌜ S i ≠ 1 ∨ X = ∅ ⌝%I as %?.
@@ -104,17 +104,17 @@ Section map.
       iDestruct (@server_1_agree with "Hs Hγ") as %?%leibniz_equiv; auto. }
     wp_select. wp_branch; wp_pures; last first.
     { iMod (@dealloc_client with "Hs Hγ") as "Hs /=".
-      wp_apply (release_spec with "[$Hlk $Hl Hc Hs]").
+      wp_smart_apply (release_spec with "[$Hlk $Hl Hc Hs]").
       { iExists i, _. iFrame. }
       iIntros "_". by iApply "HΦ". }
     wp_recv (x v) as "HI".
     iMod (@update_client with "Hs Hγ") as "[Hs Hγ]".
     { apply (gmultiset_local_update_alloc _ _ {[ x ]}). }
     rewrite left_id_L.
-    wp_apply (release_spec with "[$Hlk $Hl Hc Hs]").
+    wp_smart_apply (release_spec with "[$Hlk $Hl Hc Hs]").
     { iExists (S i), _. iFrame. }
-    clear dependent i X. iIntros "Hu". wp_apply ("Hmap" with "HI"); iIntros (l) "HI".
-    wp_apply (acquire_spec with "[$Hlk $Hu]"); iIntros "[Hl H]".
+    clear dependent i X. iIntros "Hu". wp_smart_apply ("Hmap" with "HI"); iIntros (l) "HI".
+    wp_smart_apply (acquire_spec with "[$Hlk $Hu]"); iIntros "[Hl H]".
     iDestruct "H" as (i X) "[Hs Hc]".
     iDestruct (@server_agree with "Hs Hγ")
       as %[??%gmultiset_included]; destruct i as [|i]=>//=.
@@ -123,9 +123,9 @@ Section map.
     iMod (@update_client with "Hs Hγ") as "[Hs Hγ]".
     { by apply (gmultiset_local_update_dealloc _ _ {[ x ]}). }
     rewrite gmultiset_difference_diag.
-    wp_apply (release_spec with "[$Hlk $Hl Hc Hs]").
+    wp_smart_apply (release_spec with "[$Hlk $Hl Hc Hs]").
     { iExists (S i), _. iFrame. }
-    iIntros "Hu". by wp_apply ("IH" with "[$] [$]").
+    iIntros "Hu". by wp_smart_apply ("IH" with "[$] [$]").
   Qed.
 
   Lemma par_map_workers_spec γl γ n vmap lk c :
@@ -139,10 +139,10 @@ Section map.
     iInduction n as [|n] "IH"; wp_rec; wp_pures; simpl.
     { by iApply "HΦ". }
     iDestruct "Hγs" as "[Hγ Hγs]".
-    wp_apply (wp_fork with "[Hγ]").
-    { iNext. wp_apply (par_map_worker_spec with "Hmap [$]"); auto. }
+    wp_smart_apply (wp_fork with "[Hγ]").
+    { iNext. wp_smart_apply (par_map_worker_spec with "Hmap [$]"); auto. }
     wp_pures. rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
-    wp_apply ("IH" with "[$] [$]").
+    wp_smart_apply ("IH" with "[$] [$]").
   Qed.
 
   Lemma par_map_service_spec n vmap c :
@@ -153,10 +153,10 @@ Section map.
   Proof.
     iIntros "#Hf !>"; iIntros (Φ) "Hc HΦ". wp_lam; wp_pures.
     iMod (contribution_init_pow (A:=gmultisetUR A) n) as (γ) "[Hs Hγs]".
-    wp_apply (newlock_spec (map_worker_lock_inv γ c) with "[Hc Hs]").
+    wp_smart_apply (newlock_spec (map_worker_lock_inv γ c) with "[Hc Hs]").
     { iExists n, ∅. iFrame. }
     iIntros (lk γl) "#Hlk".
-    wp_apply (par_map_workers_spec with "Hf [$Hlk $Hγs]"); auto.
+    wp_smart_apply (par_map_workers_spec with "Hf [$Hlk $Hγs]"); auto.
   Qed.
 
   Lemma par_map_client_loop_spec n c l k xs X ys :
@@ -173,18 +173,18 @@ Section map.
     { destruct Hn as [-> ->]; first lia.
       iApply ("HΦ" $! []); simpl; auto with iFrame. }
     destruct n as [|n]=> //=. wp_branch as %?|%_; wp_pures.
-    - wp_apply (lisnil_spec with "Hl"); iIntros "Hl".
+    - wp_smart_apply (lisnil_spec with "Hl"); iIntros "Hl".
       destruct xs as [|x xs]; csimpl; wp_pures.
       + wp_select. wp_pures. rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
         iApply ("IH" with "[%] Hl Hk Hc [$]"); naive_solver.
-      + wp_select. wp_apply (lpop_spec with "Hl"); iIntros (v) "[HIx Hl]".
+      + wp_select. wp_smart_apply (lpop_spec with "Hl"); iIntros (v) "[HIx Hl]".
         wp_send with "[$HIx]".
-        wp_apply ("IH" with "[] Hl Hk Hc"); first done. iIntros (ys').
+        wp_smart_apply ("IH" with "[] Hl Hk Hc"); first done. iIntros (ys').
         rewrite gmultiset_elements_disj_union gmultiset_elements_singleton.
         rewrite assoc_L -(comm _ [x]). iApply "HΦ".
     - wp_recv (x l') as (Hx) "Hl'".
-      wp_apply (lprep_spec with "[$Hk $Hl']"); iIntros "[Hk _]".
-      wp_apply ("IH" with "[] Hl Hk Hc"); first done.
+      wp_smart_apply (lprep_spec with "[$Hk $Hl']"); iIntros "[Hk _]".
+      wp_smart_apply ("IH" with "[] Hl Hk Hc"); first done.
       iIntros (ys'); iDestruct 1 as (Hys) "Hk"; simplify_eq/=.
       iApply ("HΦ" $! (ys' ++ map x)). iSplit.
       + iPureIntro. rewrite (gmultiset_disj_union_difference {[ x ]} X)
@@ -202,12 +202,12 @@ Section map.
     {{{ ys, RET #(); ⌜ys ≡ₚ xs ≫= map⌝ ∗ llist IB l ys }}}.
   Proof.
     iIntros (?) "#Hmap !>"; iIntros (Φ) "Hl HΦ". wp_lam; wp_pures.
-    wp_apply (start_chan_spec (par_map_protocol n ∅)); iIntros (c) "// Hc".
-    { wp_apply (par_map_service_spec with "Hmap Hc"); auto. }
-    wp_pures. wp_apply (lnil_spec with "[//]"); iIntros (k) "Hk".
-    wp_apply (par_map_client_loop_spec with "[$Hl $Hk $Hc //]"); first lia.
+    wp_smart_apply (start_chan_spec (par_map_protocol n ∅)); iIntros (c) "// Hc".
+    { wp_smart_apply (par_map_service_spec with "Hmap Hc"); auto. }
+    wp_pures. wp_smart_apply (lnil_spec with "[//]"); iIntros (k) "Hk".
+    wp_smart_apply (par_map_client_loop_spec with "[$Hl $Hk $Hc //]"); first lia.
     iIntros (ys) "(?&Hl&Hk)". rewrite /= gmultiset_elements_empty !right_id_L.
-    wp_apply (lapp_spec IB _ _ [] with "[$Hl $Hk]"); iIntros "[Hk _] /=".
+    wp_smart_apply (lapp_spec IB _ _ [] with "[$Hl $Hk]"); iIntros "[Hk _] /=".
     iApply "HΦ"; auto.
   Qed.
 End map.
diff --git a/theories/examples/rpc.v b/theories/examples/rpc.v
index 12b5da1bfa9a1c0c4dddb417ae7dc061bdea39dc..eefed48666cbdf340e7a828142a07b5373cd7c21 100644
--- a/theories/examples/rpc.v
+++ b/theories/examples/rpc.v
@@ -75,9 +75,9 @@ Section rpc_example.
     wp_branch; last first.
     { wp_pures. by iApply "HΦ". }
     wp_recv (T U IT IU f id) as "Hlookup".
-    wp_apply ("Hdict" with "Hlookup"); iIntros (fv) "Hfv".
+    wp_smart_apply ("Hdict" with "Hlookup"); iIntros (fv) "Hfv".
     wp_recv (x v) as "HIT".
-    wp_apply ("Hfv" with "HIT"); iIntros (w) "HIU".
+    wp_smart_apply ("Hfv" with "HIT"); iIntros (w) "HIU".
     wp_send (w) with "[$HIU]".
     wp_pures. by iApply ("IH" with "Hc").
   Qed.
@@ -128,12 +128,12 @@ Section rpc_example.
   Proof.
     iIntros (Φ) "#Hdict HΦ".
     wp_lam.
-    wp_apply (new_chan_spec (rpc_prot client_f_specs))=> //.
+    wp_smart_apply (new_chan_spec (rpc_prot client_f_specs))=> //.
     iIntros (c1 c2) "[Hc1 Hc2]".
-    wp_apply (wp_fork with "[Hc2]").
-    - iIntros "!>". wp_apply (server_spec _ _ _ END%proto with "[Hc2]").
+    wp_smart_apply (wp_fork with "[Hc2]").
+    - iIntros "!>". wp_smart_apply (server_spec _ _ _ END%proto with "[Hc2]").
       rewrite right_id. iFrame "Hdict Hc2". by iIntros "_".
-    - by wp_apply (client_spec with "Hc1").
+    - by wp_smart_apply (client_spec with "Hc1").
   Qed.
 
 End rpc_example.
diff --git a/theories/examples/sort.v b/theories/examples/sort.v
index d64765da8929d9d7937f7c69ba52b0f2049756c0..e5df3a026abdad8808fa98ffcc372a3c34b6f3ea 100644
--- a/theories/examples/sort.v
+++ b/theories/examples/sort.v
@@ -64,29 +64,29 @@ Section sort.
   Proof.
     iIntros "#Hcmp" (Ψ) "!> [Hl1 Hl2] HΨ".
     iLöb as "IH" forall (l2 xs1 xs2 Ψ).
-    wp_lam. wp_apply (lisnil_spec with "Hl1"); iIntros "Hl1".
+    wp_lam. wp_smart_apply (lisnil_spec with "Hl1"); iIntros "Hl1".
     destruct xs1 as [|x1 xs1]; wp_pures.
-    { wp_apply (lapp_spec with "[$Hl1 $Hl2]"); iIntros "[Hl1 _] /=".
+    { wp_smart_apply (lapp_spec with "[$Hl1 $Hl2]"); iIntros "[Hl1 _] /=".
       iApply "HΨ". iFrame. by rewrite list_merge_nil_l. }
-    wp_apply (lisnil_spec with "Hl2"); iIntros "Hl2".
+    wp_smart_apply (lisnil_spec with "Hl2"); iIntros "Hl2".
     destruct xs2 as [|x2 xs2]; wp_pures.
     { iApply "HΨ". by iFrame. }
-    wp_apply (lhead_spec_aux with "Hl1"); iIntros (v1 l1') "[HIx1 Hl1]".
-    wp_apply (lhead_spec_aux with "Hl2"); iIntros (v2 l2') "[HIx2 Hl2]".
-    wp_apply ("Hcmp" with "[$HIx1 $HIx2]"); iIntros "[HIx1 HIx2] /=".
+    wp_smart_apply (lhead_spec_aux with "Hl1"); iIntros (v1 l1') "[HIx1 Hl1]".
+    wp_smart_apply (lhead_spec_aux with "Hl2"); iIntros (v2 l2') "[HIx2 Hl2]".
+    wp_smart_apply ("Hcmp" with "[$HIx1 $HIx2]"); iIntros "[HIx1 HIx2] /=".
     case_bool_decide; wp_pures.
     - rewrite decide_True //.
-      wp_apply (lpop_spec_aux with "Hl1"); iIntros "Hl1".
-      wp_apply ("IH" $! _ _ (_ :: _) with "Hl1 [HIx2 Hl2]").
+      wp_smart_apply (lpop_spec_aux with "Hl1"); iIntros "Hl1".
+      wp_smart_apply ("IH" $! _ _ (_ :: _) with "Hl1 [HIx2 Hl2]").
       { iExists _, _. iFrame. }
       iIntros "Hl1".
-      wp_apply (lcons_spec with "[$Hl1 $HIx1]"). iIntros "Hl1". iApply "HΨ". iFrame.
+      wp_smart_apply (lcons_spec with "[$Hl1 $HIx1]"). iIntros "Hl1". iApply "HΨ". iFrame.
     - rewrite decide_False //.
-      wp_apply (lpop_spec_aux with "Hl2"); iIntros "Hl2".
-      wp_apply ("IH" $! _ (_ :: _) with "[HIx1 Hl1] Hl2").
+      wp_smart_apply (lpop_spec_aux with "Hl2"); iIntros "Hl2".
+      wp_smart_apply ("IH" $! _ (_ :: _) with "[HIx1 Hl1] Hl2").
       { iExists _, _. iFrame. }
       iIntros "Hl1".
-      wp_apply (lcons_spec with "[$Hl1 $HIx2]"); iIntros "Hl1". iApply "HΨ". iFrame.
+      wp_smart_apply (lcons_spec with "[$Hl1 $HIx2]"); iIntros "Hl1". iApply "HΨ". iFrame.
   Qed.
 
   Lemma sort_service_spec {A} (I : A → val → iProp Σ) (R : A → A → Prop)
@@ -98,24 +98,24 @@ Section sort.
   Proof.
     iIntros "#Hcmp !>" (Ψ) "Hc HΨ". iLöb as "IH" forall (p c Ψ). wp_lam.
     wp_recv (xs l) as "Hl".
-    wp_apply (llength_spec with "Hl"); iIntros "Hl".
+    wp_smart_apply (llength_spec with "Hl"); iIntros "Hl".
     wp_op; case_bool_decide as Hlen; wp_if.
     { assert (Sorted R xs).
       { destruct xs as [|x1 [|x2 xs]]; simpl in *; eauto with lia. }
       wp_send with "[$Hl]"; first by auto. by iApply "HΨ". }
-    wp_apply (lsplit_spec with "Hl"); iIntros (l2 vs1 vs2);
+    wp_smart_apply (lsplit_spec with "Hl"); iIntros (l2 vs1 vs2);
       iDestruct 1 as (->) "[Hl1 Hl2]".
-    wp_apply (start_chan_spec (sort_protocol I R)); iIntros (cy) "Hcy".
+    wp_smart_apply (start_chan_spec (sort_protocol I R)); iIntros (cy) "Hcy".
     { rewrite -{2}(right_id END%proto _ (iProto_dual _)).
-      wp_apply ("IH" with "Hcy"); auto. }
-    wp_apply (start_chan_spec (sort_protocol I R)); iIntros (cz) "Hcz".
+      wp_smart_apply ("IH" with "Hcy"); auto. }
+    wp_smart_apply (start_chan_spec (sort_protocol I R)); iIntros (cz) "Hcz".
     { rewrite -{2}(right_id END%proto _ (iProto_dual _)).
-      wp_apply ("IH" with "Hcz"); auto. }
+      wp_smart_apply ("IH" with "Hcz"); auto. }
     wp_send with "[$Hl1]".
     wp_send with "[$Hl2]".
     wp_recv (ys1) as (??) "Hl1".
     wp_recv (ys2) as (??) "Hl2".
-    wp_apply (lmerge_spec with "Hcmp [$Hl1 $Hl2]"); iIntros "Hl".
+    wp_smart_apply (lmerge_spec with "Hcmp [$Hl1 $Hl2]"); iIntros "Hl".
     wp_send ((list_merge R ys1 ys2)) with "[$Hl]".
     - iSplit; iPureIntro.
       + by apply (Sorted_list_merge _).
@@ -130,7 +130,7 @@ Section sort.
   Proof.
     iIntros (Ψ) "Hc HΨ". wp_lam.
     wp_recv (A I R ?? cmp) as "#Hcmp".
-    by wp_apply (sort_service_spec with "Hcmp Hc").
+    by wp_smart_apply (sort_service_spec with "Hcmp Hc").
   Qed.
 
   Lemma sort_client_func_spec {A} (I : A → val → iProp Σ) R
@@ -141,9 +141,9 @@ Section sort.
     {{{ ys, RET #(); ⌜Sorted R ys⌝ ∗ ⌜ys ≡ₚ xs⌝ ∗ llist I l ys }}}.
   Proof.
     iIntros "#Hcmp !>" (Φ) "Hl HΦ". wp_lam.
-    wp_apply (start_chan_spec sort_protocol_func); iIntros (c) "Hc".
+    wp_smart_apply (start_chan_spec sort_protocol_func); iIntros (c) "Hc".
     { rewrite -(right_id END%proto _ (iProto_dual _)).
-      wp_apply (sort_service_func_spec with "Hc"); auto. }
+      wp_smart_apply (sort_service_func_spec with "Hc"); auto. }
     wp_send with "[$Hcmp]".
     wp_send with "[$Hl]".
     wp_recv (ys) as "(Hsorted & Hperm & Hl)".
diff --git a/theories/examples/sort_br_del.v b/theories/examples/sort_br_del.v
index c153b98646f279166d491757ba2aeaeb666f5801..c628d3ea08eaea58066e47759b5499032d584b4c 100644
--- a/theories/examples/sort_br_del.v
+++ b/theories/examples/sort_br_del.v
@@ -54,8 +54,8 @@ Section sort_service_br_del.
   Proof.
     iIntros "#Hcmp !>" (Ψ) "Hc HΨ". iLöb as "IH" forall (c Ψ).
     wp_rec. wp_branch; wp_pures.
-    { wp_apply (sort_service_spec with "Hcmp Hc"); iIntros "Hc".
-      by wp_apply ("IH" with "Hc"). }
+    { wp_smart_apply (sort_service_spec with "Hcmp Hc"); iIntros "Hc".
+      by wp_smart_apply ("IH" with "Hc"). }
     by iApply "HΨ".
   Qed.
 
@@ -76,9 +76,9 @@ Section sort_service_br_del.
   Proof.
     iIntros "#Hcmp !>" (Ψ) "Hc HΨ". iLöb as "IH" forall (Ψ).
     wp_rec. wp_branch; wp_pures.
-    { wp_apply (start_chan_spec (sort_protocol I R <++> END)%proto); iIntros (c') "Hc'".
-      { wp_pures. wp_apply (sort_service_spec with "Hcmp Hc'"); auto. }
-      wp_send with "[$Hc']". by wp_apply ("IH" with "Hc"). }
+    { wp_smart_apply (start_chan_spec (sort_protocol I R <++> END)%proto); iIntros (c') "Hc'".
+      { wp_pures. wp_smart_apply (sort_service_spec with "Hcmp Hc'"); auto. }
+      wp_send with "[$Hc']". by wp_smart_apply ("IH" with "Hc"). }
     by iApply "HΨ".
   Qed.
 
@@ -99,13 +99,13 @@ Section sort_service_br_del.
   Proof.
     iIntros "#Hcmp !>" (Ψ) "Hc HΨ". iLöb as "IH" forall (c Ψ).
     wp_rec. wp_branch; wp_pures.
-    { wp_apply (sort_service_spec with "Hcmp Hc"); iIntros "Hc".
-      by wp_apply ("IH" with "Hc"). }
+    { wp_smart_apply (sort_service_spec with "Hcmp Hc"); iIntros "Hc".
+      by wp_smart_apply ("IH" with "Hc"). }
     wp_branch; wp_pures.
-    { wp_apply (start_chan_spec sort_protocol_br_del); iIntros (c') "Hc'".
-      { wp_apply ("IH" with "Hc'"); auto. }
+    { wp_smart_apply (start_chan_spec sort_protocol_br_del); iIntros (c') "Hc'".
+      { wp_smart_apply ("IH" with "Hc'"); auto. }
       wp_send with "[$Hc']".
-      by wp_apply ("IH" with "Hc"). }
+      by wp_smart_apply ("IH" with "Hc"). }
     by iApply "HΨ".
   Qed.
 End sort_service_br_del.
diff --git a/theories/examples/sort_fg.v b/theories/examples/sort_fg.v
index c8d0670b7f876acadaa2dc08f68cba7278671b72..599c12d0f59e8132bfc57c9afd57772bd23526c3 100644
--- a/theories/examples/sort_fg.v
+++ b/theories/examples/sort_fg.v
@@ -126,7 +126,7 @@ Section sort_fg.
     iIntros (Ψ) "(Hc & Hc1 & Hc2) HΨ". iLöb as "IH" forall (c c1 c2 xs xs1 xs2 Ψ).
     wp_rec. wp_branch.
     - wp_recv (x v) as "HI". wp_select. wp_send with "[$HI]".
-      wp_apply ("IH" with "Hc Hc2 Hc1").
+      wp_smart_apply ("IH" with "Hc Hc2 Hc1").
       iIntros (xs' xs1' xs2'); iDestruct 1 as (Hxs') "(Hc & Hc2 & Hc1)".
       rewrite -!(assoc_L (++)).
       iApply "HΨ". iFrame "Hc Hc1 Hc2". by rewrite Hxs' (comm (++) xs1') assoc_L.
@@ -151,7 +151,7 @@ Section sort_fg.
     wp_rec. wp_branch as %_ | %Hys'.
     - wp_recv (x v) as (Htl) "HI".
       wp_select. wp_send with "[$HI]"; first by auto.
-      wp_apply ("IH" with "[%] [%] [%] [%] Hc Hcin HΨ").
+      wp_smart_apply ("IH" with "[%] [%] [%] [%] Hc Hcin HΨ").
       * done.
       * by rewrite Hys -!assoc_L (comm _ zs).
       * auto using Sorted_snoc.
@@ -183,10 +183,10 @@ Section sort_fg.
     iLöb as "IH" forall (c1 c2 xs1 xs2 ys y1 w1 ys1 ys2 Hxs Hys Hsort Htl Htl_le).
     wp_rec. wp_branch as %_ | %Hys2.
     - wp_recv (x v) as (Htl2) "HIx".
-      wp_pures. wp_apply ("Hcmp" with "[$HIy1 $HIx]"); iIntros "[HIy1 HIx]".
+      wp_pures. wp_smart_apply ("Hcmp" with "[$HIy1 $HIx]"); iIntros "[HIy1 HIx]".
       case_bool_decide.
       + wp_select. wp_send with "[$HIy1 //]".
-        wp_apply ("IH" with "[%] [%] [%] [%] [%] Hc Hc2 Hc1 HIx HΨ").
+        wp_smart_apply ("IH" with "[%] [%] [%] [%] [%] Hc Hc2 Hc1 HIx HΨ").
         * by rewrite comm.
         * by rewrite assoc (comm _ ys2) Hys.
         * by apply Sorted_snoc.
@@ -195,14 +195,14 @@ Section sort_fg.
           inversion 1; discriminate_list || simplify_list_eq. by constructor.
       + wp_select. wp_send with "[$HIx]".
         { iPureIntro. by apply Htl_le, total_not. }
-        wp_apply ("IH" with "[% //] [%] [%] [%] [%] Hc Hc1 Hc2 HIy1 HΨ").
+        wp_smart_apply ("IH" with "[% //] [%] [%] [%] [%] Hc Hc1 Hc2 HIy1 HΨ").
         * by rewrite Hys assoc.
         * by apply Sorted_snoc, Htl_le, total_not.
         * constructor. by apply total_not.
         * intros x'.
           inversion 1; discriminate_list || simplify_list_eq. by constructor.
     - wp_select. wp_send with "[$HIy1 //]".
-      wp_apply (sort_service_fg_forward_spec with "[$Hc $Hc1]").
+      wp_smart_apply (sort_service_fg_forward_spec with "[$Hc $Hc1]").
       * done.
       * by rewrite Hys Hys2 -!assoc_L (comm _ xs2).
       * by apply Sorted_snoc.
@@ -221,19 +221,19 @@ Section sort_fg.
     wp_rec; wp_pures. wp_branch; wp_pures.
     - wp_recv (x1 v1) as "HIx1". wp_branch; wp_pures.
       + wp_recv (x2 v2) as "HIx2".
-        wp_apply (start_chan_spec (sort_fg_protocol <++> END)%proto).
-        { iIntros (cy) "Hcy". wp_apply ("IH" with "Hcy"). auto. }
+        wp_smart_apply (start_chan_spec (sort_fg_protocol <++> END)%proto).
+        { iIntros (cy) "Hcy". wp_smart_apply ("IH" with "Hcy"). auto. }
         iIntros (cy) "Hcy".
-        wp_apply (start_chan_spec (sort_fg_protocol <++> END)%proto).
-        { iIntros (cz) "Hcz". wp_apply ("IH" with "Hcz"); auto. }
+        wp_smart_apply (start_chan_spec (sort_fg_protocol <++> END)%proto).
+        { iIntros (cz) "Hcz". wp_smart_apply ("IH" with "Hcz"); auto. }
         iIntros (cz) "Hcz". rewrite !right_id.
         wp_select. wp_send with "[$HIx1]".
         wp_select. wp_send with "[$HIx2]".
-        wp_apply (sort_service_fg_split_spec with "[$Hc $Hcy $Hcz]").
+        wp_smart_apply (sort_service_fg_split_spec with "[$Hc $Hcy $Hcz]").
         iIntros (xs' xs1' xs2'); iDestruct 1 as (Hxs') "(Hc & Hcy & Hcz) /=".
         wp_branch as %_ | %[]%Permutation_nil_cons.
         wp_recv (x v) as "[_ HIx]".
-        wp_apply (sort_service_fg_merge_spec _ _ _ _ _ _ [] _ _ _ _ [] []
+        wp_smart_apply (sort_service_fg_merge_spec _ _ _ _ _ _ [] _ _ _ _ [] []
           with "Hcmp [$Hc $Hcy $Hcz $HIx]"); simpl; auto using TlRel_nil, Sorted_nil.
         by rewrite Hxs' Permutation_middle.
       + wp_select. wp_send with "[$HIx1]"; first by auto using TlRel_nil.
@@ -248,11 +248,11 @@ Section sort_fg.
   Proof.
     iIntros (Φ) "[Hl Hc] HΦ".
     iInduction xs as [|x xs] "IH" forall (xs').
-    { wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl"; wp_pures.
+    { wp_lam. wp_smart_apply (lisnil_spec with "Hl"); iIntros "Hl"; wp_pures.
       iApply "HΦ". rewrite right_id_L. by iFrame. }
-    wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl". wp_select.
-    wp_apply (lpop_spec with "Hl"); iIntros (v) "[HIx Hl]".
-    wp_send with "[$HIx]". wp_apply ("IH" with "Hl Hc"). by rewrite -assoc_L.
+    wp_lam. wp_smart_apply (lisnil_spec with "Hl"); iIntros "Hl". wp_select.
+    wp_smart_apply (lpop_spec with "Hl"); iIntros (v) "[HIx Hl]".
+    wp_send with "[$HIx]". wp_smart_apply ("IH" with "Hl Hc"). by rewrite -assoc_L.
   Qed.
 
   Lemma recv_all_spec c p l xs ys' :
@@ -267,9 +267,9 @@ Section sort_fg.
     iLöb as "IH" forall (xs ys' Φ Hsort).
     wp_lam. wp_branch as %_ | %Hperm; wp_pures.
     - wp_recv (y v) as (Htl) "HIx".
-      wp_apply ("IH" with "[] Hl Hc"); first by auto using Sorted_snoc.
+      wp_smart_apply ("IH" with "[] Hl Hc"); first by auto using Sorted_snoc.
       iIntros (ys). rewrite -!assoc_L. iDestruct 1 as (??) "[Hl Hc]".
-      wp_apply (lcons_spec with "[$Hl $HIx]"); iIntros "Hl".
+      wp_smart_apply (lcons_spec with "[$Hl $HIx]"); iIntros "Hl".
       iApply ("HΦ" with "[$Hl $Hc]"); simpl; eauto.
     - iApply ("HΦ" $! []); rewrite /= right_id_L; by iFrame.
   Qed.
@@ -281,11 +281,11 @@ Section sort_fg.
     {{{ ys, RET #(); ⌜Sorted R ys⌝ ∗ ⌜ys ≡ₚ xs⌝ ∗ llist I l ys }}}.
   Proof.
     iIntros "#Hcmp !>" (Φ) "Hl HΦ". wp_lam.
-    wp_apply (start_chan_spec (sort_fg_protocol <++> END)%proto); iIntros (c) "Hc".
-    { wp_apply (sort_service_fg_spec with "Hcmp Hc"); auto. }
-    wp_apply (send_all_spec with "[$Hl $Hc]"); iIntros "[Hl Hc]".
+    wp_smart_apply (start_chan_spec (sort_fg_protocol <++> END)%proto); iIntros (c) "Hc".
+    { wp_smart_apply (sort_service_fg_spec with "Hcmp Hc"); auto. }
+    wp_smart_apply (send_all_spec with "[$Hl $Hc]"); iIntros "[Hl Hc]".
     wp_select.
-    wp_apply (recv_all_spec with "[$Hl $Hc]"); auto.
+    wp_smart_apply (recv_all_spec with "[$Hl $Hc]"); auto.
     iIntros (ys) "/=". iDestruct 1 as (??) "[Hk _]".
     iApply "HΦ"; auto with iFrame.
   Qed.
@@ -305,6 +305,6 @@ Section sort_fg.
   Proof.
     iIntros (Ψ) "Hc HΨ". wp_lam.
     wp_recv (A I R ? ? cmp) as "#Hcmp".
-    by wp_apply (sort_service_fg_spec with "Hcmp Hc").
+    by wp_smart_apply (sort_service_fg_spec with "Hcmp Hc").
   Qed.
 End sort_fg.
diff --git a/theories/examples/swap_mapper.v b/theories/examples/swap_mapper.v
index 0b21edf08005ced29ad2e2e569f80847fcfdf3ed..cbb3df7c485708a16708ebafeada792c528f03a5 100644
--- a/theories/examples/swap_mapper.v
+++ b/theories/examples/swap_mapper.v
@@ -220,12 +220,12 @@ Section with_Σ.
   Proof.
     iIntros (Φ) "[Hl Hc] HΦ".
     iInduction xs as [|x xs] "IH" forall (xs').
-    { wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl"; wp_pures.
+    { wp_lam. wp_smart_apply (lisnil_spec with "Hl"); iIntros "Hl"; wp_pures.
       iApply "HΦ". by iFrame. }
-    wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl".
+    wp_lam. wp_smart_apply (lisnil_spec with "Hl"); iIntros "Hl".
     wp_send with "[//]".
-    wp_apply (lpop_spec with "Hl"); iIntros (v) "[HIx Hl]".
-    wp_send with "[$HIx]". wp_apply ("IH" with "Hl Hc"). simpl.
+    wp_smart_apply (lpop_spec with "Hl"); iIntros (v) "[HIx Hl]".
+    wp_send with "[$HIx]". wp_smart_apply ("IH" with "Hl Hc"). simpl.
     by rewrite -assoc_L.
   Qed.
 
@@ -248,9 +248,9 @@ Section with_Σ.
     wp_lam. wp_recv (w) as "Hw". wp_pures.
     rewrite Nat2Z.inj_succ.
     replace (Z.succ (Z.of_nat (length xs)) - 1)%Z with (Z.of_nat (length xs)) by lia.
-    wp_apply ("IH" with "Hl Hc").
+    wp_smart_apply ("IH" with "Hl Hc").
     iIntros (ys) "(% & Hl & Hc)".
-    wp_apply (lcons_spec with "[$Hl $Hw]").
+    wp_smart_apply (lcons_spec with "[$Hl $Hw]").
     iIntros "Hl". iApply "HΦ". iFrame. iPureIntro. by f_equiv.
   Qed.
 
@@ -359,7 +359,7 @@ Section with_Σ.
     iIntros "#Hfspec !>" (Φ) "Hc HΦ".
     iLöb as "IH".
     wp_rec. wp_branch.
-    - wp_recv (x v) as "HT". wp_apply ("Hfspec" with "HT").
+    - wp_recv (x v) as "HT". wp_smart_apply ("Hfspec" with "HT").
       iIntros (w) "HU".
       wp_send with "[$HU]". wp_pures. iApply ("IH" with "Hc HΦ").
     - wp_pures. by iApply "HΦ".
@@ -373,17 +373,17 @@ Section with_Σ.
   Proof.
     iIntros "#Hfspec !>" (Φ) "HIT HΦ".
     wp_lam.
-    wp_apply (start_chan_spec mapper_prot); iIntros (c) "// Hc".
+    wp_smart_apply (start_chan_spec mapper_prot); iIntros (c) "// Hc".
     { wp_lam. rewrite -(iProto_app_end_r (iProto_dual mapper_prot)).
       iApply (swap_mapper_service_spec _ _ END%proto with "Hfspec Hc").
       auto. }
-    wp_apply (llength_spec with "HIT"); iIntros "HIT".
-    wp_apply (send_all_spec with "[$HIT Hc]").
+    wp_smart_apply (llength_spec with "HIT"); iIntros "HIT".
+    wp_smart_apply (send_all_spec with "[$HIT Hc]").
     { iApply (iProto_mapsto_le with "Hc").
       iApply subprot_n_swap. }
     iIntros "[HIT Hc]".
     rewrite right_id rev_involutive.
-    wp_apply (recv_all_spec with "[$HIT $Hc]").
+    wp_smart_apply (recv_all_spec with "[$HIT $Hc]").
     iIntros (ys) "(% & HIT & Hc)".
     wp_select.
     iApply "HΦ".
diff --git a/theories/logrel/examples/compute_client_list.v b/theories/logrel/examples/compute_client_list.v
index 86fb796d5be02ca2224b5f4556cfde4f61bfe0a7..4e675a80b71c2ec208408ad2a29b4eac8c22fb74 100644
--- a/theories/logrel/examples/compute_client_list.v
+++ b/theories/logrel/examples/compute_client_list.v
@@ -167,9 +167,9 @@ Section compute_example.
   Proof.
     iIntros (Φ) "(Hl & Hf & #Hlk) HΦ".
     iInduction xs as [|x xs] "IH".
-    { wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl".
+    { wp_lam. wp_smart_apply (lisnil_spec with "Hl"); iIntros "Hl".
       rewrite /select.
-      wp_apply (acquire_spec with "Hlk").
+      wp_smart_apply (acquire_spec with "Hlk").
       iIntros "[Hlocked HI]".
       iDestruct "HI" as (n [ | ]) "(Hf' & Hcounter & Hc)"; last first.
       { by iDestruct (own_valid_2 with "Hf Hf'") as %[]. }
@@ -182,14 +182,14 @@ Section compute_example.
         iApply lty_napp_swap.
         iApply recv_type_stop_type_swap. }
       wp_send with "[]"; [ eauto | ].
-      wp_apply (release_spec with "[-HΦ Hl]").
+      wp_smart_apply (release_spec with "[-HΦ Hl]").
       { iFrame "Hlk Hlocked".
         iExists n, false.
         rewrite lookup_total_insert -lsty_car_app lty_app_end_l lty_app_end_r.
         iFrame "Hf Hcounter Hc". }
       iIntros "_". iApply "HΦ". by iFrame "Hl Hlk". }
-    wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl".
-    wp_apply (acquire_spec with "Hlk").
+    wp_lam. wp_smart_apply (lisnil_spec with "Hl"); iIntros "Hl".
+    wp_smart_apply (acquire_spec with "Hlk").
     iIntros "[Hlocked HI]".
     iDestruct "HI" as (n [ | ]) "(Hf' & Hcounter & Hc)"; last first.
     { by iDestruct (own_valid_2 with "Hf Hf'") as %[]. }
@@ -207,11 +207,11 @@ Section compute_example.
     rewrite /select.
     wp_send with "[]"; [ eauto | ].
     rewrite lookup_total_insert.
-    wp_apply (lpop_spec with "Hl"); iIntros (v) "[HIx Hl]".
+    wp_smart_apply (lpop_spec with "Hl"); iIntros (v) "[HIx Hl]".
     wp_send with "[HIx]".
     { iDestruct "HIx" as (->) "$HIx". }
     wp_load. wp_store.
-    wp_apply (release_spec with "[-HΦ Hf Hl]").
+    wp_smart_apply (release_spec with "[-HΦ Hf Hl]").
     { iFrame "Hlk Hlocked".
       iExists (n+1), true.
       rewrite assoc.
@@ -241,12 +241,12 @@ Section compute_example.
     destruct n as [ | n ].
     { wp_lam. wp_pures. iApply "HΦ". by iFrame "Hl Hlk". }
     wp_lam.
-    wp_apply (acquire_spec with "Hlk").
+    wp_smart_apply (acquire_spec with "Hlk").
     iIntros "[Hlocked HI]".
     iDestruct "HI" as (m b) "(Hb & Hcounter & Hc)".
     wp_load.
     destruct m as [ | m ].
-    { wp_apply (release_spec with "[$Hlocked $Hlk Hb Hcounter Hc]").
+    { wp_smart_apply (release_spec with "[$Hlocked $Hlk Hb Hcounter Hc]").
       { iExists 0, b. iFrame "Hb Hcounter Hc". }
       iIntros "_". wp_pures. iApply ("IH" with "Hl").
       iApply "HΦ". }
@@ -254,15 +254,15 @@ Section compute_example.
     rewrite Nat2Z.inj_succ.
     wp_load. wp_store.
     replace (Z.succ (Z.of_nat m) - 1)%Z with (Z.of_nat m) by lia.
-    wp_apply (release_spec with "[$Hlocked $Hlk Hb Hcounter Hc]").
+    wp_smart_apply (release_spec with "[$Hlocked $Hlk Hb Hcounter Hc]").
     { replace (Z.succ (Z.of_nat m) - 1)%Z with (Z.of_nat m) by lia.
       iExists m, b. iFrame "Hb Hcounter Hc". }
     iIntros "_".
     wp_pures.
     replace (Z.of_nat (S n) - 1)%Z with (Z.of_nat (n)) by lia.
-    wp_apply ("IH" with "Hl").
+    wp_smart_apply ("IH" with "Hl").
     iIntros (ys). iDestruct 1 as (Heq) "(Hl & Hc)".
-    wp_apply (lcons_spec with "[$Hl $Hw//]").
+    wp_smart_apply (lcons_spec with "[$Hl $Hw//]").
     iIntros "Hl". iApply "HΦ". iFrame.
     iPureIntro. by rewrite Heq.
   Qed.
@@ -281,25 +281,25 @@ Section compute_example.
     iDestruct (ctx_ltyped_cons _ _ "xs" with "HΓ") as (vlxs ->) "[Hlxs HΓ]".
     rewrite /lty_list /lty_rec fixpoint_unfold.
     iDestruct "Hlxs" as (l' v ->) "[Hlxs Hv]".
-    wp_apply (llength_spec with "[Hlxs Hv]").
+    wp_smart_apply (llength_spec with "[Hlxs Hv]").
     { iEval (rewrite /lty_list /lty_rec fixpoint_unfold).
       iExists l', v. eauto with iFrame. }
     iIntros (xs n) "[<- Hlxs]".
     wp_alloc counter as "Hcounter".
-    wp_apply (lnil_spec); [ done | ].
+    wp_smart_apply (lnil_spec); [ done | ].
     iIntros (lys) "Hlys".
     iMod (own_alloc 1%Qp) as (γf) "Hf"; [ done | ].
-    wp_apply (newlock_spec (compute_type_invariant γf A vc counter)
+    wp_smart_apply (newlock_spec (compute_type_invariant γf A vc counter)
                 with "[Hcounter Hc]").
     { iExists 0, true. repeat rewrite left_id. iFrame "Hcounter Hc". }
     iIntros (lk γ) "#Hlk".
-    wp_apply (par_spec
+    wp_smart_apply (par_spec
                 (λ v, ⌜v = #()⌝)%I
                 (λ v, ∃ ys, ⌜v = #()⌝ ∗ llist (llist_type_pred A) lys ys)%I
                 with "[Hlxs Hf] [Hlys]").
-    { wp_apply (send_all_par_spec with "[$Hlxs $Hf $Hlk]").
+    { wp_smart_apply (send_all_par_spec with "[$Hlxs $Hf $Hlk]").
       iIntros "(Hlxs & _)". eauto. }
-    { wp_apply (recv_all_par_spec with "[$Hlys $Hlk]").
+    { wp_smart_apply (recv_all_par_spec with "[$Hlys $Hlk]").
       iIntros (ys) "(Heq & Hlys & _)".
       iExists ys. iFrame. eauto. }
     iIntros (w1 w2) "[-> Hw2]".
diff --git a/theories/logrel/examples/mapper_list.v b/theories/logrel/examples/mapper_list.v
index 1703f718bfccd638929f704f4aa488051dba567c..7c57be0a628024f3be1b832230a1fa5d190d3a8f 100644
--- a/theories/logrel/examples/mapper_list.v
+++ b/theories/logrel/examples/mapper_list.v
@@ -244,16 +244,16 @@ Section mapper_example.
   Proof.
     iIntros (Φ) "[Hl Hc] HΦ".
     iInduction xs as [|x xs] "IH".
-    { wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl"; wp_pures.
+    { wp_lam. wp_smart_apply (lisnil_spec with "Hl"); iIntros "Hl"; wp_pures.
       iApply "HΦ". by iFrame. }
-    wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl".
+    wp_lam. wp_smart_apply (lisnil_spec with "Hl"); iIntros "Hl".
     rewrite /select.
     wp_send with "[]"; first by eauto.
     rewrite lookup_total_insert.
-    wp_apply (lpop_spec with "Hl"); iIntros (v) "[HIx Hl]".
+    wp_smart_apply (lpop_spec with "Hl"); iIntros (v) "[HIx Hl]".
     wp_send with "[HIx]".
     { iDestruct "HIx" as (->) "$HIx". }
-    wp_apply ("IH" with "Hl Hc").
+    wp_smart_apply ("IH" with "Hl Hc").
     done.
   Qed.
 
@@ -267,19 +267,19 @@ Section mapper_example.
   Proof.
     iIntros (Φ) "[Hl Hc] HΦ".
     iInduction xs as [|x xs] "IH" forall (n).
-    { wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl"; wp_pures.
+    { wp_lam. wp_smart_apply (lisnil_spec with "Hl"); iIntros "Hl"; wp_pures.
       iApply "HΦ". by iFrame. }
-    wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl".
+    wp_lam. wp_smart_apply (lisnil_spec with "Hl"); iIntros "Hl".
     simpl.
     iDestruct (iProto_mapsto_le c with "Hc []") as "Hc".
     { iApply recv_mapper_type_rec_client_unfold_app. }
     rewrite /select.
     wp_send with "[]"; first by eauto.
     rewrite lookup_total_insert.
-    wp_apply (lpop_spec with "Hl"); iIntros (v) "[HIx Hl]".
+    wp_smart_apply (lpop_spec with "Hl"); iIntros (v) "[HIx Hl]".
     wp_send with "[HIx]".
     { iDestruct "HIx" as (->) "$HIx". }
-    wp_apply ("IH" $!(S n) with "Hl Hc").
+    wp_smart_apply ("IH" $!(S n) with "Hl Hc").
     by rewrite Nat.add_succ_r.
   Qed.
 
@@ -312,9 +312,9 @@ Section mapper_example.
     wp_lam. wp_recv (w) as "Hw". wp_pures.
     rewrite Nat2Z.inj_succ.
     replace (Z.succ (Z.of_nat (n)) - 1)%Z with (Z.of_nat (n)) by lia.
-    wp_apply ("IH" with "Hl Hc").
+    wp_smart_apply ("IH" with "Hl Hc").
     iIntros (ys) "(% & Hl & Hc)".
-    wp_apply (lcons_spec with "[$Hl $Hw//]").
+    wp_smart_apply (lcons_spec with "[$Hl $Hw//]").
     iIntros "Hl". iApply "HΦ". iFrame.
     iPureIntro. by rewrite H1.
   Qed.
@@ -338,12 +338,12 @@ Section mapper_example.
     iDestruct (ctx_ltyped_cons _ _ "f" with "HΓ") as (vf ->) "[Hf HΓ]".
     wp_send with "[Hf//]".
     iDestruct (list_type_loc with "Hl") as %[l ->].
-    wp_apply (llength_spec A with "Hl").
+    wp_smart_apply (llength_spec A with "Hl").
     iIntros (xs n) "[<- Hl]".
     wp_pures.
-    wp_apply (send_all_spec_ad_hoc with "[$Hl $Hc]").
+    wp_smart_apply (send_all_spec_ad_hoc with "[$Hl $Hc]").
     iIntros "[Hl Hc]".
-    wp_apply (recv_all_spec with "[Hl $Hc //]").
+    wp_smart_apply (recv_all_spec with "[Hl $Hc //]").
     iIntros (ys). iDestruct 1 as (Hlen) "[Hl Hc]".
     rewrite /mapper_type_rec_client /lty_rec fixpoint_unfold.
     rewrite /select.
@@ -372,14 +372,14 @@ Section mapper_example.
     iDestruct (ctx_ltyped_cons _ _ "f" with "HΓ") as (vf ->) "[Hf HΓ]".
     wp_send with "[Hf//]".
     iDestruct (list_type_loc with "Hl") as %[l ->].
-    wp_apply (llength_spec with "Hl").
+    wp_smart_apply (llength_spec with "Hl").
     iIntros (xs n) "[<- Hl]".
     wp_pures.
     iDestruct (iProto_mapsto_le vc with "Hc []") as "Hc".
     { iApply (mapper_type_rec_client_unfold_app_n A B (length xs)). }
-    wp_apply (send_all_spec_upfront with "[$Hl $Hc]").
+    wp_smart_apply (send_all_spec_upfront with "[$Hl $Hc]").
     iIntros "[Hl Hc]".
-    wp_apply (recv_all_spec with "[Hl $Hc //]").
+    wp_smart_apply (recv_all_spec with "[Hl $Hc //]").
     iIntros (ys). iDestruct 1 as (Hlen) "[Hl Hc]".
     rewrite /mapper_type_rec_client /lty_rec fixpoint_unfold.
     rewrite /select.
diff --git a/theories/logrel/examples/par_recv.v b/theories/logrel/examples/par_recv.v
index 6c932d4d84a51f20519f8120d97c5d367e47566e..3f8e65424636a2f9b7c5cf96134f3995b4a5bf84 100755
--- a/theories/logrel/examples/par_recv.v
+++ b/theories/logrel/examples/par_recv.v
@@ -53,44 +53,44 @@ Section double.
     rewrite /prog.
     iMod (own_alloc 1%Qp) as (γ) "[Hcredit1 Hcredit2]"; [done|].
     (* Create lock *)
-    wp_apply (newlock_spec (chan_inv c γ) with "[Hc]").
+    wp_smart_apply (newlock_spec (chan_inv c γ) with "[Hc]").
     { iLeft. iFrame "Hc". }
     iIntros (lk γlk) "#Hlock".
     wp_pures.
     (* Fork into two threads *)
-    wp_apply (wp_par (λ v, ∃ k : Z, ⌜v = #k⌝)%I (λ v, ∃ k : Z, ⌜v = #k⌝)%I
+    wp_smart_apply (wp_par (λ v, ∃ k : Z, ⌜v = #k⌝)%I (λ v, ∃ k : Z, ⌜v = #k⌝)%I
                 with "[Hcredit1] [Hcredit2]").
     - (* Acquire lock *)
-      wp_apply (acquire_spec with "Hlock").
+      wp_smart_apply (acquire_spec with "Hlock").
       iIntros "[Hlocked Hc]". wp_pures.
       iDestruct "Hc" as "[Hc|[Hc|Hc]]".
       + wp_recv (x1) as "_". wp_pures.
-        wp_apply (release_spec with "[Hlocked Hcredit1 Hc]").
+        wp_smart_apply (release_spec with "[Hlocked Hcredit1 Hc]").
         { iFrame "Hlock Hlocked". iRight. iLeft. iFrame "Hcredit1 Hc". }
         iIntros "_". wp_pures.
         eauto.
       + iDestruct "Hc" as "[Hcredit2 Hc]".
         wp_recv (x1) as "_". wp_pures.
         iCombine "Hcredit1 Hcredit2" as "Hcredit".
-        wp_apply (release_spec with "[Hlocked Hcredit Hc]").
+        wp_smart_apply (release_spec with "[Hlocked Hcredit Hc]").
         { iFrame "Hlock Hlocked". iRight. iRight. iFrame "Hcredit Hc". }
         iIntros "_". wp_pures.
         eauto.
       + iDestruct "Hc" as "[Hcredit2 Hc]".
         by iDestruct (own_valid_2 with "Hcredit1 Hcredit2") as %[].
     - (* Acquire lock *)
-      wp_apply (acquire_spec with "Hlock").
+      wp_smart_apply (acquire_spec with "Hlock").
       iIntros "[Hlocked Hc]". wp_pures.
       iDestruct "Hc" as "[Hc|[Hc|Hc]]".
       + wp_recv (x1) as "_". wp_pures.
-        wp_apply (release_spec with "[Hlocked Hcredit2 Hc]").
+        wp_smart_apply (release_spec with "[Hlocked Hcredit2 Hc]").
         { iFrame "Hlock Hlocked". iRight. iLeft. iFrame "Hcredit2 Hc". }
         iIntros "_". wp_pures.
         eauto.
       + iDestruct "Hc" as "[Hcredit1 Hc]".
         wp_recv (x1) as "Hx1". wp_pures.
         iCombine "Hcredit1 Hcredit2" as "Hcredit".
-        wp_apply (release_spec with "[Hlocked Hcredit Hc]").
+        wp_smart_apply (release_spec with "[Hlocked Hcredit Hc]").
         { iFrame "Hlock Hlocked". iRight. iRight. iFrame "Hcredit Hc". }
         iIntros "_". wp_pures.
         eauto.
@@ -143,11 +143,11 @@ Section double_fc.
     iMod (own_alloc (1, to_agree None)%Qp) as (γ1) "Hγ1"; [done|].
     iMod (own_alloc (1, to_agree None)%Qp) as (γ2) "Hγ2"; [done|].
     (* Create lock *)
-    wp_apply (newlock_spec (chan_inv_fc γ γ1 γ2 P c) with "[Hγ Hc]").
+    wp_smart_apply (newlock_spec (chan_inv_fc γ γ1 γ2 P c) with "[Hγ Hc]").
     { iLeft. by iFrame. }
     iIntros (lk γlk) "#Hlock". wp_pures.
     (* Fork into two threads *)
-    wp_apply (wp_par
+    wp_smart_apply (wp_par
       (λ v1, own γ1 (1/4, to_agree (Some v1))%Qp ∗ own γ (Excl ()) ∨
         (∃ v2, own γ1 (3/4, to_agree (Some v1))%Qp ∗
                own γ2 (1/2, to_agree (Some v2))%Qp ∗ P v2 v1))%I
@@ -155,13 +155,13 @@ Section double_fc.
         (∃ v1, own γ2 (3/4, to_agree (Some v2))%Qp ∗
                own γ1 (1/2, to_agree (Some v1))%Qp ∗ P v1 v2))%I with "[Hγ1] [Hγ2]").
     - (* Acquire lock *)
-      wp_apply (acquire_spec with "Hlock").
+      wp_smart_apply (acquire_spec with "Hlock").
       iIntros "[Hlocked Hc]". wp_pures.
       iDestruct "Hc" as "[[Hγ Hc]|[Hc|Hc]]".
       + wp_recv (v) as "_". wp_pures.
         iMod (own_update _ _ ((3/4 ⋅ 1/4), to_agree (Some v))%Qp with "Hγ1")
           as "[Hγ1a Hγ1b]"; [by apply cmra_update_exclusive|].
-        wp_apply (release_spec with "[$Hlock $Hlocked Hγ1a Hc]").
+        wp_smart_apply (release_spec with "[$Hlock $Hlocked Hγ1a Hc]").
         { iRight. iLeft. iExists true, v. iFrame. }
         iIntros "_". wp_pures. iLeft. by iFrame.
       + iDestruct "Hc" as ([] v) "[Hγ2 Hc]".
@@ -171,19 +171,19 @@ Section double_fc.
           as "[Hγ1a Hγ1b]"; [by apply cmra_update_exclusive|].
         rewrite {1}(_ : 3/4 = 1/4 + 1/2)%Qp; last (by apply: bool_decide_unpack).
         iDestruct "Hγ2" as "[Hγ2a Hγ2b]".
-        wp_apply (release_spec with "[$Hlock $Hlocked Hγ1a Hγ2a Hc]").
+        wp_smart_apply (release_spec with "[$Hlock $Hlocked Hγ1a Hγ2a Hc]").
         { do 2 iRight. iExists v', v. iFrame. }
         iIntros "_". wp_pures. iRight. iExists v. by iFrame.
       + iDestruct "Hc" as (v v') "[Hγ1' _]".
         by iDestruct (own_valid_2 with "Hγ1 Hγ1'") as %[].
     - (* Acquire lock *)
-      wp_apply (acquire_spec with "Hlock").
+      wp_smart_apply (acquire_spec with "Hlock").
       iIntros "[Hlocked Hc]". wp_pures.
       iDestruct "Hc" as "[[Hγ Hc]|[Hc|Hc]]".
       + wp_recv (v) as "_". wp_pures.
         iMod (own_update _ _ ((3/4 ⋅ 1/4), to_agree (Some v))%Qp with "Hγ2")
           as "[Hγ2a Hγ2b]"; [by apply cmra_update_exclusive|].
-        wp_apply (release_spec with "[$Hlock $Hlocked Hγ2a Hc]").
+        wp_smart_apply (release_spec with "[$Hlock $Hlocked Hγ2a Hc]").
         { iRight. iLeft. iExists false, v. iFrame. }
         iIntros "_". wp_pures. iLeft. by iFrame.
       + iDestruct "Hc" as ([] v) "[Hγ1 Hc]"; last first.
@@ -193,7 +193,7 @@ Section double_fc.
           as "[Hγ2a Hγ2b]"; [by apply cmra_update_exclusive|].
         rewrite {1}(_ : 3/4 = 1/4 + 1/2)%Qp; last (by apply: bool_decide_unpack).
         iDestruct "Hγ1" as "[Hγ1a Hγ1b]".
-        wp_apply (release_spec with "[$Hlock $Hlocked Hγ1a Hγ2a Hc]").
+        wp_smart_apply (release_spec with "[$Hlock $Hlocked Hγ1a Hγ2a Hc]").
         { do 2 iRight. iExists v, v'. iFrame. }
         iIntros "_". wp_pures. iRight. iExists v. by iFrame.
       + iDestruct "Hc" as (v v') "(_ & Hγ2' & _)".
diff --git a/theories/logrel/lib/list.v b/theories/logrel/lib/list.v
index 6f14340c87c2c4df0823d653fea82fd3894df9be..4ee66b8fba95b06a2df9451e552afdab68dfcaf8 100644
--- a/theories/logrel/lib/list.v
+++ b/theories/logrel/lib/list.v
@@ -61,7 +61,7 @@ Section with_Σ.
       wp_pures.
       rewrite fixpoint_unfold.
       iDestruct "Hl'" as (l' xs ->) "[Hl' Hl'']".
-      wp_apply ("IH" with "[Hl' Hl'']").
+      wp_smart_apply ("IH" with "[Hl' Hl'']").
       { rewrite /lty_list /lty_rec.
         iEval (rewrite fixpoint_unfold).
         iExists _, _. iFrame "Hl' Hl''". done. }
diff --git a/theories/logrel/lib/mutex.v b/theories/logrel/lib/mutex.v
index 02d2ee1b19f6388885aa165c78ecf1cad3296e84..47b1065e5c3870dce7b0693dac1d0c16d1e67720 100644
--- a/theories/logrel/lib/mutex.v
+++ b/theories/logrel/lib/mutex.v
@@ -110,7 +110,7 @@ Section rules.
     set (N := nroot .@ "makelock").
     iAssert (∃ inner, l ↦ inner ∗ ltty_car A inner)%I with "[Hl Hv]" as "Hlock".
     { iExists v. iFrame "Hl Hv". }
-    wp_apply (newlock_spec with "Hlock").
+    wp_smart_apply (newlock_spec with "Hlock").
     iIntros (lk γ) "Hlock".
     wp_pures. iExists γ, l, lk. eauto.
   Qed.
@@ -122,7 +122,7 @@ Section rules.
     iIntros (HΓx%ctx_lookup_perm vs) "!> HΓ /=". rewrite {1}HΓx /=.
     iDestruct (ctx_ltyped_cons with "HΓ") as (vl Hvs) "[Hlock HΓ]"; rewrite Hvs.
     iDestruct "Hlock" as (γ l lk ->) "#Hlock". rewrite /mutex_acquire.
-    wp_apply (acquire_spec with "Hlock"); iIntros "[Hlocked Hinner]".
+    wp_smart_apply (acquire_spec with "Hlock"); iIntros "[Hlocked Hinner]".
     iDestruct "Hinner" as (v) "[Hl HA]".
     wp_load. iFrame "HA". iApply ctx_ltyped_cons.
     iFrame "HΓ". iModIntro. iExists _; iSplit; [done|]. iExists γ, l, lk, v. auto with iFrame.
@@ -134,7 +134,7 @@ Section rules.
     (Γ ⊨ mutex_release x e : () ⫤ ctx_cons x (mutex A) Γ').
   Proof.
     iIntros (HΓx%ctx_lookup_perm) "#He". iIntros (vs) "!> HΓ /=".
-    wp_apply (wp_wand with "(He HΓ)"). iIntros (v) "[HA HΓ']".
+    wp_smart_apply (wp_wand with "(He HΓ)"). iIntros (v) "[HA HΓ']".
     rewrite {2}HΓx /=.
     iDestruct (ctx_ltyped_cons with "HΓ'") as (vl Hvs) "[Hguard HΓ']"; rewrite Hvs.
     iDestruct "Hguard" as (γ l lk inner ->) "(#Hlock & Hlocked & Hinner)".
@@ -142,7 +142,7 @@ Section rules.
     iAssert (∃ inner, l ↦ inner ∗ ltty_car A inner)%I
       with "[Hinner HA]" as "Hinner".
     { iExists v. iFrame "Hinner HA". }
-    wp_apply (release_spec γ _ (∃ inner, l ↦ inner ∗ ltty_car A inner)%I
+    wp_smart_apply (release_spec γ _ (∃ inner, l ↦ inner ∗ ltty_car A inner)%I
       with "[$Hlock $Hlocked $Hinner]").
     iIntros "_". iSplit; [done|].
     iApply ctx_ltyped_cons. iFrame "HΓ'". iExists _; iSplit; [done|].
diff --git a/theories/logrel/session_typing_rules.v b/theories/logrel/session_typing_rules.v
index 584ecd0a02cf184fe699884a9cacf158fd348bde..1a2b24d4c37120026e58e1697761af497e3c154f 100644
--- a/theories/logrel/session_typing_rules.v
+++ b/theories/logrel/session_typing_rules.v
@@ -31,7 +31,7 @@ Section session_typing_rules.
     (Γ ⊨ send x e : () ⫤ ctx_cons x (chan S) Γ').
   Proof.
     iIntros (HΓx%ctx_lookup_perm) "#He !>". iIntros (vs) "HΓ /=".
-    wp_apply (wp_wand with "(He HΓ)"); iIntros (v) "[HA HΓ']".
+    wp_smart_apply (wp_wand with "(He HΓ)"); iIntros (v) "[HA HΓ']".
     rewrite {2}HΓx /=.
     iDestruct (ctx_ltyped_cons with "HΓ'") as (c Hvs) "[Hc HΓ']". rewrite Hvs.
     wp_send with "[HA //]". iSplitR; [done|].
@@ -94,7 +94,7 @@ Section session_typing_rules.
     { iApply (iProto_mapsto_le with "Hc"); iIntros "!>". rewrite HM.
       iApply iProto_le_lmsg_texist. }
     wp_recv (Xs v) as "HA". wp_pures. rewrite -subst_map_binder_insert.
-    wp_apply (wp_wand with "(He [- HΓ1eq])").
+    wp_smart_apply (wp_wand with "(He [- HΓ1eq])").
     { iApply (ctx_ltyped_insert _ _ x with "HA").
       destruct (decide (x = xc)) as [->|].
       - by rewrite ctx_filter_ne_cons.
@@ -145,7 +145,7 @@ Section session_typing_rules.
     iIntros "H". wp_pures. iIntros "!>" (v) "HA".
     iDestruct ("H" with "HA") as "H".
     rewrite subst_map_insert.
-    wp_apply "H".
+    wp_smart_apply "H".
   Qed.
 
   Lemma lty_arr_list_spec As (e : expr) B ws y i n :
diff --git a/theories/logrel/term_typing_rules.v b/theories/logrel/term_typing_rules.v
index da08a29eb1d3edc98e5456ce4e8f75191513331e..6cc22f35496bba653d7a9106f21504f4956b1467 100644
--- a/theories/logrel/term_typing_rules.v
+++ b/theories/logrel/term_typing_rules.v
@@ -79,7 +79,7 @@ Section term_typing_rules.
     (Γ1 ⊨ UnOp op e : B ⫤ Γ2).
   Proof.
     iIntros (Hop) "#He !>". iIntros (vs) "HΓ1 /=".
-    wp_apply (wp_wand with "(He [HΓ1 //])"). iIntros (v1) "[HA $]".
+    wp_smart_apply (wp_wand with "(He [HΓ1 //])"). iIntros (v1) "[HA $]".
     iDestruct (Hop with "HA") as (w ?) "HB". by wp_unop.
   Qed.
 
@@ -90,8 +90,8 @@ Section term_typing_rules.
     (Γ1 ⊨ BinOp op e1 e2 : B ⫤ Γ3).
   Proof.
     iIntros (Hop) "#He2 #He1 !>". iIntros (vs) "HΓ1 /=".
-    wp_apply (wp_wand with "(He2 [HΓ1 //])"). iIntros (v2) "[HA2 HΓ2]".
-    wp_apply (wp_wand with "(He1 [HΓ2 //])"). iIntros (v1) "[HA1 $]".
+    wp_smart_apply (wp_wand with "(He2 [HΓ1 //])"). iIntros (v2) "[HA2 HΓ2]".
+    wp_smart_apply (wp_wand with "(He1 [HΓ2 //])"). iIntros (v1) "[HA1 $]".
     iDestruct (Hop with "HA1 HA2") as (w ?) "HB". by wp_binop.
   Qed.
 
@@ -103,10 +103,10 @@ Section term_typing_rules.
     (Γ1 ⊨ (if: e1 then e2 else e3) : A ⫤ Γ3).
   Proof.
     iIntros "#He1 #He2 #He3 !>" (v) "HΓ1 /=".
-    wp_apply (wp_wand with "(He1 [HΓ1 //])"). iIntros (b) "[Hbool HΓ2]".
+    wp_smart_apply (wp_wand with "(He1 [HΓ1 //])"). iIntros (b) "[Hbool HΓ2]".
     rewrite /lty_bool. iDestruct "Hbool" as ([]) "->".
-    - wp_apply (wp_wand with "(He2 [HΓ2 //])"). iIntros (w) "[$$]".
-    - wp_apply (wp_wand with "(He3 [HΓ2 //])"). iIntros (w) "[$$]".
+    - wp_smart_apply (wp_wand with "(He2 [HΓ2 //])"). iIntros (w) "[$$]".
+    - wp_smart_apply (wp_wand with "(He3 [HΓ2 //])"). iIntros (w) "[$$]".
   Qed.
 
   (** Arrow properties *)
@@ -115,8 +115,8 @@ Section term_typing_rules.
     (Γ1 ⊨ e1 e2 : A2 ⫤ Γ3).
   Proof.
     iIntros "#H2 #H1". iIntros (vs) "!> HΓ /=".
-    wp_apply (wp_wand with "(H2 [HΓ //])"). iIntros (v) "[HA1 HΓ]".
-    wp_apply (wp_wand with "(H1 [HΓ //])"). iIntros (f) "[Hf $]".
+    wp_smart_apply (wp_wand with "(H2 [HΓ //])"). iIntros (v) "[HA1 HΓ]".
+    wp_smart_apply (wp_wand with "(H1 [HΓ //])"). iIntros (f) "[Hf $]".
     iApply ("Hf" $! v with "HA1").
   Qed.
 
@@ -125,8 +125,8 @@ Section term_typing_rules.
     (Γ1 ⊨ e1 e2 : A2 ⫤ Γ3).
   Proof.
     iIntros "#H2 #H1". iIntros (vs) "!> HΓ /=".
-    wp_apply (wp_wand with "(H2 [HΓ //])"). iIntros (v) "[HA1 HΓ]".
-    wp_apply (wp_wand with "(H1 [HΓ //])"). iIntros (f) "[Hf HΓ]".
+    wp_smart_apply (wp_wand with "(H2 [HΓ //])"). iIntros (v) "[HA1 HΓ]".
+    wp_smart_apply (wp_wand with "(H1 [HΓ //])"). iIntros (f) "[Hf HΓ]".
     iApply wp_frame_r. iFrame "HΓ". iApply ("Hf" $! v with "HA1").
   Qed.
 
@@ -205,7 +205,7 @@ Section term_typing_rules.
     (Γ1 ⊨ (let: x:=e1 in e2) : A2 ⫤ ctx_filter_eq x Γ2 ++ ctx_filter_ne x Γ3).
   Proof.
     iIntros "#He1 #He2 !>". iIntros (vs) "HΓ1 /=".
-    wp_apply (wp_wand with "(He1 HΓ1)"); iIntros (v) "[HA1 HΓ2]". wp_pures.
+    wp_smart_apply (wp_wand with "(He1 HΓ1)"); iIntros (v) "[HA1 HΓ2]". wp_pures.
     rewrite {3}(ctx_filter_eq_perm Γ2 x).
     iDestruct (ctx_ltyped_app with "HΓ2") as "[HΓ2eq HΓ2neq]".
     iDestruct ("He2" $! (binder_insert x v vs) with "[HA1 HΓ2neq]") as "He'".
@@ -221,8 +221,8 @@ Section term_typing_rules.
     (Γ1 ⊨ (e1 ;; e2) : B ⫤ Γ3).
   Proof.
     iIntros "#He1 #He2 !>". iIntros (vs) "HΓ1 /=".
-    wp_apply (wp_wand with "(He1 HΓ1)"); iIntros (v) "[_ HΓ2]". wp_pures.
-    wp_apply (wp_wand with "(He2 HΓ2)"); iIntros (w) "[HB HΓ3]".
+    wp_smart_apply (wp_wand with "(He1 HΓ1)"); iIntros (v) "[_ HΓ2]". wp_pures.
+    wp_smart_apply (wp_wand with "(He2 HΓ2)"); iIntros (w) "[HB HΓ3]".
     iFrame "HB HΓ3".
   Qed.
 
@@ -232,8 +232,8 @@ Section term_typing_rules.
     (Γ1 ⊨ (e1,e2) : A1 * A2 ⫤ Γ3).
   Proof.
     iIntros "#H2 #H1". iIntros (vs) "!> HΓ /=".
-    wp_apply (wp_wand with "(H2 [HΓ //])"); iIntros (w2) "[HA2 HΓ]".
-    wp_apply (wp_wand with "(H1 [HΓ //])"); iIntros (w1) "[HA1 HΓ]".
+    wp_smart_apply (wp_wand with "(H2 [HΓ //])"); iIntros (w2) "[HA2 HΓ]".
+    wp_smart_apply (wp_wand with "(H1 [HΓ //])"); iIntros (w1) "[HA1 HΓ]".
     wp_pures. iFrame "HΓ". iExists w1, w2. by iFrame.
   Qed.
 
@@ -267,7 +267,7 @@ Section term_typing_rules.
     (Γ1 ⊨ InjL e : A1 + A2 ⫤ Γ2).
   Proof.
     iIntros "#HA" (vs) "!> HΓ /=".
-    wp_apply (wp_wand with "(HA [HΓ //])").
+    wp_smart_apply (wp_wand with "(HA [HΓ //])").
     iIntros (v) "[HA' $]". wp_pures.
     iLeft. iExists v. auto.
   Qed.
@@ -277,7 +277,7 @@ Section term_typing_rules.
     (Γ1 ⊨ InjR e : A1 + A2 ⫤ Γ2).
   Proof.
     iIntros "#HA" (vs) "!> HΓ /=".
-    wp_apply (wp_wand with "(HA [HΓ //])").
+    wp_smart_apply (wp_wand with "(HA [HΓ //])").
     iIntros (v) "[HA' $]". wp_pures.
     iRight. iExists v. auto.
   Qed.
@@ -289,11 +289,11 @@ Section term_typing_rules.
     (Γ1 ⊨ Case e1 e2 e3 : B ⫤ Γ3).
   Proof.
     iIntros "#H1 #H2 #H3" (vs) "!> HΓ1 /=".
-    wp_apply (wp_wand with "(H1 HΓ1)"). iIntros (s) "[[Hs|Hs] HΓ2]";
+    wp_smart_apply (wp_wand with "(H1 HΓ1)"). iIntros (s) "[[Hs|Hs] HΓ2]";
       iDestruct "Hs" as (w ->) "HA"; wp_case.
-    - wp_apply (wp_wand with "(H2 HΓ2)"). iIntros (v) "[Hv $]".
+    - wp_smart_apply (wp_wand with "(H2 HΓ2)"). iIntros (v) "[Hv $]".
       iApply (wp_wand with "(Hv HA)"). auto.
-    - wp_apply (wp_wand with "(H3 HΓ2)"). iIntros (v) "[Hv $]".
+    - wp_smart_apply (wp_wand with "(H3 HΓ2)"). iIntros (v) "[Hv $]".
       iApply (wp_wand with "(Hv HA)"). auto.
   Qed.
 
@@ -313,7 +313,7 @@ Section term_typing_rules.
     (Γ ⊨ e #() : C K ⫤ Γ2).
   Proof.
     iIntros "#He" (vs) "!> HΓ /=".
-    wp_apply (wp_wand with "(He [HΓ //])"); iIntros (w) "[HB HΓ] /=".
+    wp_smart_apply (wp_wand with "(He [HΓ //])"); iIntros (w) "[HB HΓ] /=".
     iApply (wp_wand with "HB [HΓ]"). by iIntros (v) "$".
   Qed.
 
@@ -322,7 +322,7 @@ Section term_typing_rules.
     (Γ1 ⊨ e : C K ⫤ Γ2) -∗ Γ1 ⊨ e : (∃ X, C X) ⫤ Γ2.
   Proof.
     iIntros "#He" (vs) "!> HΓ /=".
-    wp_apply (wp_wand with "(He [HΓ //])"); iIntros (w) "[HB $]". by iExists K.
+    wp_smart_apply (wp_wand with "(He [HΓ //])"); iIntros (w) "[HB $]". by iExists K.
   Qed.
 
   Lemma ltyped_unpack {k} Γ1 Γ2 Γ3 x e1 e2 (C : lty Σ k → ltty Σ) B :
@@ -331,7 +331,7 @@ Section term_typing_rules.
     (Γ1 ⊨ (let: x := e1 in e2) : B ⫤ ctx_filter_eq x Γ2 ++ ctx_filter_ne x Γ3).
   Proof.
     iIntros "#He1 #He2 !>". iIntros (vs) "HΓ1 /=".
-    wp_apply (wp_wand with "(He1 HΓ1)"); iIntros (v) "[HC HΓ2]".
+    wp_smart_apply (wp_wand with "(He1 HΓ1)"); iIntros (v) "[HC HΓ2]".
     iDestruct "HC" as (X) "HX". wp_pures.
     rewrite {3}(ctx_filter_eq_perm Γ2 x).
     iDestruct (ctx_ltyped_app with "HΓ2") as "[HΓ2eq HΓ2neq]".
@@ -348,7 +348,7 @@ Section term_typing_rules.
     (Γ1 ⊨ ref e : ref_uniq A ⫤ Γ2).
   Proof.
     iIntros "#He" (vs) "!> HΓ1 /=".
-    wp_apply (wp_wand with "(He HΓ1)"). iIntros (v) "[Hv $]".
+    wp_smart_apply (wp_wand with "(He HΓ1)"). iIntros (v) "[Hv $]".
     wp_alloc l as "Hl". iExists l, v; eauto with iFrame.
   Qed.
 
@@ -357,7 +357,7 @@ Section term_typing_rules.
     (Γ1 ⊨ Free e : () ⫤ Γ2).
   Proof.
     iIntros "#He" (vs) "!> HΓ1 /=".
-    wp_apply (wp_wand with "(He HΓ1)"). iIntros (v) "[Hv $]".
+    wp_smart_apply (wp_wand with "(He HΓ1)"). iIntros (v) "[Hv $]".
     iDestruct "Hv" as (l w ->) "[Hl Hw]". by wp_free.
   Qed.
 
@@ -379,7 +379,7 @@ Section term_typing_rules.
     (Γ ⊨ x <- e : () ⫤ ctx_cons x (ref_uniq B) Γ').
   Proof.
     iIntros (HΓx%ctx_lookup_perm) "#He"; iIntros (vs) "!> HΓ /=".
-    wp_apply (wp_wand with "(He HΓ)"). iIntros (v) "[HB HΓ']".
+    wp_smart_apply (wp_wand with "(He HΓ)"). iIntros (v) "[HB HΓ']".
     rewrite {2}HΓx /=.
     iDestruct (ctx_ltyped_cons with "HΓ'") as (vl Hvs) "[HA HΓ']"; rewrite Hvs.
     iDestruct "HA" as (l w ->) "[? HA]". wp_store. iModIntro. iSplit; [done|].
@@ -405,7 +405,7 @@ Section term_typing_rules.
     Γ ⊨ ! e : A ⫤ Γ'.
   Proof.
     iIntros "#He" (vs) "!> HΓ /=".
-    wp_apply (wp_wand with "(He HΓ)"). iIntros (v) "[Hv $]".
+    wp_smart_apply (wp_wand with "(He HΓ)"). iIntros (v) "[Hv $]".
     iDestruct "Hv" as (l ->) "#Hv".
     iInv (ref_shrN .@ l) as (v) "[>Hl #HA]" "Hclose".
     wp_load.
@@ -419,7 +419,7 @@ Section term_typing_rules.
     (Γ1 ⊨ e1 <- e2 : () ⫤ Γ3).
   Proof.
     iIntros "#H1 #H2" (vs) "!> HΓ1 /=".
-    wp_apply (wp_wand with "(H1 HΓ1)"). iIntros (v) "[Hv HΓ2]".
+    wp_smart_apply (wp_wand with "(H1 HΓ1)"). iIntros (v) "[Hv HΓ2]".
     wp_bind (subst_map vs e1).
     iApply (wp_wand with "(H2 HΓ2)"). iIntros (w) "[Hw $]".
     iDestruct "Hw" as (l ->) "#Hw".
@@ -434,8 +434,8 @@ Section term_typing_rules.
     (Γ1 ⊨ FAA e1 e2 : lty_int ⫤ Γ3).
   Proof.
     iIntros "#H1 #H2" (vs) "!> HΓ1 /=".
-    wp_apply (wp_wand with "(H1 HΓ1)"). iIntros (v) "[Hv HΓ2]".
-    wp_apply (wp_wand with "(H2 HΓ2)"). iIntros (w) "[Hw $]".
+    wp_smart_apply (wp_wand with "(H1 HΓ1)"). iIntros (v) "[Hv HΓ2]".
+    wp_smart_apply (wp_wand with "(H2 HΓ2)"). iIntros (w) "[Hw $]".
     iDestruct "Hw" as (l ->) "#Hw".
     iInv (ref_shrN .@ l) as (w) "[Hl >Hn]" "Hclose".
     iDestruct "Hn" as %[k ->].
@@ -454,7 +454,7 @@ Section term_typing_rules.
   Proof.
     iIntros "#He1 #He2 !>" (vs) "HΓ /=".
     iDestruct (ctx_ltyped_app with "HΓ") as "[HΓ1 HΓ2]".
-    wp_apply (wp_par with "(He1 HΓ1) (He2 HΓ2)").
+    wp_smart_apply (wp_par with "(He1 HΓ1) (He2 HΓ2)").
     iIntros (v1 v2) "[[HA HΓ1'] [HB HΓ2']] !>". iSplitL "HA HB".
     + iExists v1, v2. by iFrame.
     + iApply ctx_ltyped_app. by iFrame.
diff --git a/theories/utils/llist.v b/theories/utils/llist.v
index 0428f6b0f85a2127af989ea3fe4e76bf589edce4..533f0e300e6aade86a0787c8871848f74469847b 100644
--- a/theories/utils/llist.v
+++ b/theories/utils/llist.v
@@ -150,7 +150,7 @@ Lemma lhead_spec l x xs :
     lhead #l
   {{{ v, RET v; I x v ∗ (I x v -∗ llist I l (x :: xs)) }}}.
 Proof.
-  iIntros (Φ) "Hll HΦ". wp_apply (lhead_spec_aux with "Hll").
+  iIntros (Φ) "Hll HΦ". wp_smart_apply (lhead_spec_aux with "Hll").
   iIntros (v l') "(HIx&?&?)". iApply "HΦ". iIntros "{$HIx} HIx".
   simpl; eauto with iFrame.
 Qed.
@@ -159,7 +159,7 @@ Lemma lpop_spec l x xs :
   {{{ llist I l (x :: xs) }}} lpop #l {{{ v, RET v; I x v ∗ llist I l xs }}}.
 Proof.
   iIntros (Φ) "/=". iDestruct 1 as (v l') "(HIx & Hl & Hll)". iIntros "HΦ".
-  wp_apply (lpop_spec_aux with "[$]"); iIntros "Hll". iApply "HΦ"; iFrame.
+  wp_smart_apply (lpop_spec_aux with "[$]"); iIntros "Hll". iApply "HΦ"; iFrame.
 Qed.
 
 Lemma llookup_spec l i xs x :
@@ -171,11 +171,11 @@ Proof.
   iIntros (Hi Φ) "Hll HΦ".
   iInduction xs as [|x' xs] "IH" forall (l i x Hi Φ); [done|simpl; wp_rec; wp_pures].
   destruct i as [|i]; simplify_eq/=; wp_pures.
-  - wp_apply (lhead_spec with "Hll"); iIntros (v) "[HI Hll]".
+  - wp_smart_apply (lhead_spec with "Hll"); iIntros (v) "[HI Hll]".
     iApply "HΦ"; eauto with iFrame.
   - iDestruct "Hll" as (v l') "(HIx' & Hl' & Hll)". wp_load; wp_pures.
     rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
-    wp_apply ("IH" with "[//] Hll"); iIntros (v') "[HIx Hll]".
+    wp_smart_apply ("IH" with "[//] Hll"); iIntros (v') "[HIx Hll]".
     iApply "HΦ". iIntros "{$HIx} HIx". iExists v, l'. iFrame. by iApply "Hll".
 Qed.
 
@@ -186,7 +186,7 @@ Proof.
   iInduction xs as [|x xs] "IH" forall (l Φ); simpl; wp_rec; wp_pures.
   - wp_load; wp_pures. by iApply "HΦ".
   - iDestruct "Hll" as (v l') "(HIx & Hl' & Hll)". wp_load; wp_pures.
-    wp_apply ("IH" with "Hll"); iIntros "Hll". wp_pures.
+    wp_smart_apply ("IH" with "Hll"); iIntros "Hll". wp_pures.
     rewrite (Nat2Z.inj_add 1). iApply "HΦ"; eauto with iFrame.
 Qed.
 
@@ -202,7 +202,7 @@ Proof.
     + iDestruct "Hll2" as (v2 l2') "(HIx2 & Hl2 & Hll2)". wp_load. wp_store.
       iApply "HΦ". iSplitR "Hl2"; eauto 10 with iFrame.
   - iDestruct "Hll1" as (v1 l') "(HIx1 & Hl1 & Hll1)". wp_load; wp_pures.
-    wp_apply ("IH" with "Hll1 Hll2"); iIntros "[Hll Hl2]".
+    wp_smart_apply ("IH" with "Hll1 Hll2"); iIntros "[Hll Hl2]".
     iApply "HΦ"; eauto with iFrame.
 Qed.
 
@@ -212,7 +212,7 @@ Lemma lprep_spec l1 l2 xs1 xs2 :
   {{{ RET #(); llist I l1 (xs1 ++ xs2) ∗ (∃ v, l2 ↦ v) }}}.
 Proof.
   iIntros (Φ) "[Hll1 Hll2] HΦ". wp_lam.
-  wp_apply (lapp_spec with "[$Hll2 $Hll1]"); iIntros "[Hll2 Hl1]".
+  wp_smart_apply (lapp_spec with "[$Hll2 $Hll1]"); iIntros "[Hll2 Hl1]".
   iDestruct "Hl1" as (w) "Hl1". destruct (xs1 ++ xs2) as [|x xs]; simpl; wp_pures.
   - wp_load. wp_store. iApply "HΦ"; eauto with iFrame.
   - iDestruct "Hll2" as (v l') "(HIx & Hl2 & Hll2)". wp_load. wp_store.
@@ -226,7 +226,7 @@ Proof.
   iInduction xs as [|x' xs] "IH" forall (l Φ); simpl; wp_rec; wp_pures.
   - wp_load. wp_alloc k. wp_store. iApply "HΦ"; eauto with iFrame.
   - iDestruct "Hll" as (v' l') "(HIx' & Hl & Hll)". wp_load; wp_pures.
-    wp_apply ("IH" with "Hll HIx"); iIntros "Hll". iApply "HΦ"; eauto with iFrame.
+    wp_smart_apply ("IH" with "Hll HIx"); iIntros "Hll". iApply "HΦ"; eauto with iFrame.
 Qed.
 
 Lemma lsplit_at_spec l xs (n : nat) :
@@ -242,7 +242,7 @@ Proof.
   - iDestruct "Hll" as (v l') "(HIx & Hl & Hll)". destruct n as [|n]; simpl; wp_pures.
     + wp_load. wp_alloc k. wp_store. iApply "HΦ"; eauto with iFrame.
     + wp_load; wp_pures. rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
-      wp_apply ("IH" with "[$]"); iIntros (k) "[Hll Hlk]".
+      wp_smart_apply ("IH" with "[$]"); iIntros (k) "[Hll Hlk]".
       iApply "HΦ"; eauto with iFrame.
 Qed.
 
@@ -252,9 +252,9 @@ Lemma lsplit_spec l xs :
   {{{ k xs1 xs2, RET #k; ⌜ xs = xs1 ++ xs2 ⌝ ∗ llist I l xs1 ∗ llist I k xs2 }}}.
 Proof.
   iIntros (Φ) "Hl HΦ". wp_lam.
-  wp_apply (llength_spec with "Hl"); iIntros "Hl". wp_pures.
+  wp_smart_apply (llength_spec with "Hl"); iIntros "Hl". wp_pures.
   rewrite Z.quot_div_nonneg; [|lia..]. rewrite -(Nat2Z_inj_div _ 2).
-  wp_apply (lsplit_at_spec with "Hl"); iIntros (k) "[Hl Hk]".
+  wp_smart_apply (lsplit_at_spec with "Hl"); iIntros (k) "[Hl Hk]".
   iApply "HΦ". iFrame. by rewrite take_drop.
 Qed.
 
@@ -267,8 +267,8 @@ Proof.
   iInduction xs as [|x xs] "IH" forall (l acc Φ ys).
   - wp_lam. wp_load. wp_pures. iApply "HΦ". rewrite app_nil_l. iApply "Hacc".
   - wp_lam. iDestruct "Hl" as (v l') "[HI [Hl Hl']]".
-    wp_load. wp_apply (lcons_spec with "[$Hacc $HI]").
-    iIntros "Hacc". wp_apply ("IH" with "Hl' Hacc").
+    wp_load. wp_smart_apply (lcons_spec with "[$Hacc $HI]").
+    iIntros "Hacc". wp_smart_apply ("IH" with "Hl' Hacc").
     iIntros (l'') "Hl''". iApply "HΦ".
     rewrite reverse_cons -app_assoc. iApply "Hl''".
 Qed.
@@ -281,17 +281,17 @@ Proof.
   iIntros (Φ) "Hl HΦ". wp_lam.
   destruct xs.
   - wp_load. wp_alloc l' as "Hl'".
-    wp_apply (lnil_spec)=> //.
+    wp_smart_apply (lnil_spec)=> //.
     iIntros (lnil) "Hlnil".
     iAssert (llist I l' []) with "Hl'" as "Hl'".
-    wp_apply (lreverse_at_spec with "[$Hl' $Hlnil]").
+    wp_smart_apply (lreverse_at_spec with "[$Hl' $Hlnil]").
     iIntros (l'') "Hl''".
     wp_load. wp_store. iApply "HΦ". rewrite app_nil_r. iApply "Hl".
   - iDestruct "Hl" as (v lcons) "[HI [Hlcons Hrec]]".
     wp_load. wp_alloc l' as "Hl'".
-    wp_apply (lnil_spec)=> //.
+    wp_smart_apply (lnil_spec)=> //.
     iIntros (lnil) "Hlnil".
-    wp_apply (lreverse_at_spec _ (a::xs) with "[Hl' HI Hrec Hlnil]").
+    wp_smart_apply (lreverse_at_spec _ (a::xs) with "[Hl' HI Hrec Hlnil]").
     { iFrame "Hlnil". iExists v, lcons. iFrame. }
     iIntros (l'') "Hl''".
     assert (∃ ys, ys = reverse (a :: xs)) as [ys Hys].