diff --git a/tests/ipm_paper.ref b/tests/ipm_paper.ref
index 9bcb74f82069801b5c48be7eae96fc66eb070ff9..5bfcbbd9faa239cd9679ec008a67fe148904b19a 100644
--- a/tests/ipm_paper.ref
+++ b/tests/ipm_paper.ref
@@ -9,8 +9,8 @@
   x : A
   ============================
   "HP" : P
-  "HΨ" : Ψ x
   "HR" : R
+  "HΨ" : Ψ x
   --------------------------------------∗
   Ψ x ∗ P
   
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index df2cc9712695a348b65241118b0cc74435b34347..89f0aee35c083931ec657d4c5aadde2ccc9a69c1 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -555,10 +555,9 @@ In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
 "tac" (bound to spec_tac ltac:(()); [ .. | tac Htmp ]), 
 "tac" (bound to fun H => iDestructHyp H as pat),
 "iDestructHyp (constr) as (constr)",
-"<iris.proofmode.ltac_tactics.iDestructHypFindPat>",
-"<iris.proofmode.ltac_tactics.iDestructHypGo>" and
-"iRename (constr) into (constr)", last call failed.
-Tactic failure: iRename: "H" not fresh.
+"<iris.proofmode.ltac_tactics.iDestructHypFindPat>" and
+"iFastDestructHyp (constr) as (constr)", last call failed.
+Tactic failure: iDestruct: given names not fresh.
 "iPoseProof_not_found_fail"
      : string
 The command has indeed failed with message:
@@ -602,8 +601,9 @@ In nested Ltac calls to "iDestruct (open_constr) as (constr)",
 "iDestructCore (open_constr) as (constr) (tactic)", 
 "tac" (bound to fun H => iDestructHyp H as pat),
 "iDestructHyp (constr) as (constr)",
-"<iris.proofmode.ltac_tactics.iDestructHypFindPat>" and
-"<iris.proofmode.ltac_tactics.iDestructHypGo>", last call failed.
+"<iris.proofmode.ltac_tactics.iDestructHypFindPat>",
+"iFastDestructHyp (constr) as (constr)" and
+"<iris.proofmode.ltac_tactics.iFastDestructHypGo>", last call failed.
 Tactic failure: iDestruct: (IList [[IClear (sel_patterns.SelIdent "HP")]])
 invalid.
 "iOrDestruct_fail"
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 07af70c40f1bc7f1d439e3d07f9c7986a5822042..e21ea2095059fc5a8b74d0da421de003cdeb3185 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -261,7 +261,7 @@ Proof. iIntros "H". iNext. done. Qed.
 
 Lemma test_iFrame_persistent (P Q : PROP) :
   □ P -∗ Q -∗ <pers> (P ∗ P) ∗ (P ∗ Q ∨ Q).
-Proof. iIntros "#HP". iFrame "HP". iIntros "$". Qed.
+Proof. iIntros "#HP". iFrame "HP". by iIntros "$". Qed.
 
 Lemma test_iSplit_persistently P Q : □ P -∗ <pers> (P ∗ P).
 Proof. iIntros "#?". by iSplit. Qed.
@@ -321,7 +321,7 @@ Qed.
 
 Lemma test_iIntros_let P :
   ∀ Q, let R := emp%I in P -∗ R -∗ Q -∗ P ∗ Q.
-Proof. iIntros (Q R) "$ _ $". Qed.
+Proof. by iIntros (Q R) "$ _ $". Qed.
 
 Lemma test_iNext_iRewrite P Q : <affine> ▷ (Q ≡ P) -∗ <affine> ▷ Q -∗ <affine> ▷ P.
 Proof.
@@ -565,18 +565,18 @@ Proof. iIntros "HP" (Q) "_ #HPQ". by iApply "HPQ". Qed.
 Lemma test_and_sep (P Q R : PROP) : P ∧ (Q ∗ □ R) ⊢ (P ∧ Q) ∗ □ R.
 Proof.
   iIntros "H". repeat iSplit.
-  - iDestruct "H" as "[$ _]".
-  - iDestruct "H" as "[_ [$ _]]".
-  - iDestruct "H" as "[_ [_ #$]]".
+  - by iDestruct "H" as "[$ _]".
+  - by iDestruct "H" as "[_ [$ _]]".
+  - by iDestruct "H" as "[_ [_ #$]]".
 Qed.
 
 Lemma test_and_sep_2 (P Q R : PROP) `{!Persistent R, !Affine R} :
   P ∧ (Q ∗ R) ⊢ (P ∧ Q) ∗ R.
 Proof.
   iIntros "H". repeat iSplit.
-  - iDestruct "H" as "[$ _]".
-  - iDestruct "H" as "[_ [$ _]]".
-  - iDestruct "H" as "[_ [_ #$]]".
+  - by iDestruct "H" as "[$ _]".
+  - by iDestruct "H" as "[_ [$ _]]".
+  - by iDestruct "H" as "[_ [_ #$]]".
 Qed.
 
 Check "test_and_sep_affine_bi".
diff --git a/tests/proofmode_iris.ref b/tests/proofmode_iris.ref
index 0dbca72f4bf79e467472c44b99700f3542570f5c..6db6be4f340eac3a4bde0bc76c5f30ad02a31560 100644
--- a/tests/proofmode_iris.ref
+++ b/tests/proofmode_iris.ref
@@ -60,8 +60,8 @@
   _ : cinv N γ (<pers> P)
   "HP" : â–· <pers> P
   --------------------------------------â–¡
-  "Hown" : cinv_own γ p
   "Hclose" : ▷ <pers> P ={⊤ ∖ ↑N,⊤}=∗ emp
+  "Hown" : cinv_own γ p
   --------------------------------------∗
   |={⊤ ∖ ↑N,⊤}=> cinv_own γ p ∗ ▷ P
   
@@ -102,8 +102,8 @@
   "HP" : â–· <pers> P
   --------------------------------------â–¡
   "Hown1" : na_own t E1
-  "Hown2" : na_own t (E2 ∖ ↑N)
   "Hclose" : ▷ <pers> P ∗ na_own t (E2 ∖ ↑N) ={⊤}=∗ na_own t E2
+  "Hown2" : na_own t (E2 ∖ ↑N)
   --------------------------------------∗
   |={⊤}=> na_own t E1 ∗ na_own t E2 ∗ ▷ P
   
@@ -155,8 +155,8 @@ Tactic failure: iInv: invariant "H2" not found.
   𝓟 : iProp Σ
   H : ↑N ⊆ E
   ============================
-  "HP" : ⎡ ▷ 𝓟 ⎤
   "Hclose" : ⎡ ▷ 𝓟 ={E ∖ ↑N,E}=∗ emp ⎤
+  "HP" : ⎡ ▷ 𝓟 ⎤
   --------------------------------------∗
   |={E ∖ ↑N,E}=> emp
   
diff --git a/tests/proofmode_iris.v b/tests/proofmode_iris.v
index d369d746b6567fcb2c05a8e16b8108df65dffdb8..241b084231b74798a77ac7da0a386c575dab294a 100644
--- a/tests/proofmode_iris.v
+++ b/tests/proofmode_iris.v
@@ -40,13 +40,13 @@ Section base_logic_tests.
   Proof. iIntros. iAssert False%I with "[> - //]" as %[]. Qed.
 
   Lemma test_iStartProof_1 P : P -∗ P.
-  Proof. iStartProof. iStartProof. iIntros "$". Qed.
+  Proof. iStartProof. iStartProof. by iIntros "$". Qed.
   Lemma test_iStartProof_2 P : P -∗ P.
-  Proof. iStartProof (uPred _). iStartProof (uPredI _). iIntros "$". Qed.
+  Proof. iStartProof (uPred _). iStartProof (uPredI _). by iIntros "$". Qed.
   Lemma test_iStartProof_3 P : P -∗ P.
-  Proof. iStartProof (uPredI _). iStartProof (uPredSI _). iIntros "$". Qed.
+  Proof. iStartProof (uPredI _). iStartProof (uPredSI _). by iIntros "$". Qed.
   Lemma test_iStartProof_4 P : P -∗ P.
-  Proof. iStartProof (uPredSI _). iStartProof (uPred _). iIntros "$". Qed.
+  Proof. iStartProof (uPredSI _). iStartProof (uPred _). by iIntros "$". Qed.
 End base_logic_tests.
 
 Section iris_tests.
diff --git a/tests/proofmode_monpred.v b/tests/proofmode_monpred.v
index a88a79168cee626a47e0994a368d1e295df2f151..8fb73f42ae894eeba4dc6ba805641ada59ec4e76 100644
--- a/tests/proofmode_monpred.v
+++ b/tests/proofmode_monpred.v
@@ -11,20 +11,20 @@ Section tests.
   Implicit Types i j : I.
 
   Lemma test0 P : P -∗ P.
-  Proof. iIntros "$". Qed.
+  Proof. by iIntros "$". Qed.
 
   Lemma test_iStartProof_1 P : P -∗ P.
-  Proof. iStartProof. iStartProof. iIntros "$". Qed.
+  Proof. iStartProof. iStartProof. by iIntros "$". Qed.
   Lemma test_iStartProof_2 P : P -∗ P.
-  Proof. iStartProof monPred. iStartProof monPredI. iIntros "$". Qed.
+  Proof. iStartProof monPred. iStartProof monPredI. by iIntros "$". Qed.
   Lemma test_iStartProof_3 P : P -∗ P.
-  Proof. iStartProof monPredI. iStartProof monPredSI. iIntros "$". Qed.
+  Proof. iStartProof monPredI. iStartProof monPredSI. by iIntros "$". Qed.
   Lemma test_iStartProof_4 P : P -∗ P.
-  Proof. iStartProof monPredSI. iStartProof monPred. iIntros "$". Qed.
+  Proof. iStartProof monPredSI. iStartProof monPred. by iIntros "$". Qed.
   Lemma test_iStartProof_5 P : P -∗ P.
-  Proof. iStartProof PROP. iIntros (i) "$". Qed.
+  Proof. iStartProof PROP. by iIntros (i) "$". Qed.
   Lemma test_iStartProof_6 P : P ⊣⊢ P.
-  Proof. iStartProof PROP. iIntros (i). iSplit; iIntros "$". Qed.
+  Proof. iStartProof PROP. iIntros (i). iSplit; by iIntros "$". Qed.
   Lemma test_iStartProof_7 P : ((P ≡ P)%I : monPredI).
   Proof. iStartProof PROP. done. Qed.
 
@@ -58,11 +58,11 @@ Section tests.
 
   Lemma test_iStartProof_forall_1 (Φ : nat → monPredI) : ∀ n, Φ n -∗ Φ n.
   Proof.
-    iStartProof PROP. iIntros (n i) "$".
+    iStartProof PROP. by iIntros (n i) "$".
   Qed.
   Lemma test_iStartProof_forall_2 (Φ : nat → monPredI) : ∀ n, Φ n -∗ Φ n.
   Proof.
-    iStartProof. iIntros (n) "$".
+    iStartProof. by iIntros (n) "$".
   Qed.
 
   Lemma test_embed_wand (P Q : PROP) : (⎡P⎤ -∗ ⎡Q⎤) -∗ ⎡P -∗ Q⎤ : monPred.
@@ -160,7 +160,7 @@ Section tests.
 
   Lemma test_iFrame_embed (P : PROP) i :
     P -∗ (embed (B:=monPredI) P) i.
-  Proof. iIntros "$". Qed.
+  Proof. by iIntros "$". Qed.
 
   (* Make sure search doesn't diverge on an evar *)
   Lemma test_iFrame_monPred_at_evar (P : monPred) i j :
diff --git a/theories/base_logic/lib/na_invariants.v b/theories/base_logic/lib/na_invariants.v
index c92594bf03bd69529cc77263d2a513d64c3fe8ef..bf16cadbc9cf5601dff4cb1029525037f1cfa7ba 100644
--- a/theories/base_logic/lib/na_invariants.v
+++ b/theories/base_logic/lib/na_invariants.v
@@ -48,7 +48,7 @@ Section proofs.
     iIntros "#HPQ". rewrite /na_inv. iDestruct 1 as (i ?) "#Hinv".
     iExists i. iSplit; first done. iApply (inv_iff with "[] Hinv").
     iNext; iAlways.
-    iSplit; iIntros "[[? Ho]|$]"; iLeft; iFrame "Ho"; by iApply "HPQ".
+    iSplit; iIntros "[[? Ho]|$] //"; iLeft; iFrame "Ho"; by iApply "HPQ".
   Qed.
 
   Lemma na_alloc : (|==> ∃ p, na_own p ⊤)%I.
diff --git a/theories/heap_lang/lib/spawn.v b/theories/heap_lang/lib/spawn.v
index a213fec88bfa18f4926cb90472bb32f0af781c66..6069724ef838be7396b6b67f543995e0fbd0e449 100644
--- a/theories/heap_lang/lib/spawn.v
+++ b/theories/heap_lang/lib/spawn.v
@@ -66,7 +66,7 @@ Proof.
   iLöb as "IH". wp_rec. wp_bind (! _)%E. iInv N as (v) "[Hl Hinv]".
   wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
   - iModIntro. iSplitL "Hl"; [iNext; iExists _; iFrame; eauto|].
-    wp_apply ("IH" with "Hγ [HΦ]"). auto.
+    wp_apply ("IH" with "[HΦ] Hγ"). auto.
   - iDestruct "Hinv" as (v' ->) "[HΨ|Hγ']".
     + iModIntro. iSplitL "Hl Hγ"; [iNext; iExists _; iFrame; eauto|].
       wp_pures. by iApply "HΦ".
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index fbfb2a7ce89453d12370a4e1a5366226ceaefe0a..318d012a1ab75a2e24a8c7289ac96e41fff8672f 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -715,6 +715,170 @@ Proof.
   - setoid_rewrite <-(right_id emp%I _ (Pout _)). auto.
 Qed.
 
+(** * Delayed tactics *)
+Local Notation of_env_temps tmps :=
+  ([∗ list] tmp ∈ tmps, of_env_temp tmp)%I.
+Local Notation of_env_actions acts :=
+  ([∗ list] act ∈ acts, of_env_action act)%I.
+
+Lemma envs_entails_delayed_unfold Δ acts tmps Q :
+  envs_entails_delayed Δ acts tmps Q ↔
+    (of_env_temps tmps ∗ of_env_actions acts ∗ of_envs Δ ⊢ Q).
+Proof.
+  rewrite /envs_entails_delayed envs_entails_eq. split.
+  - intros ->. by rewrite assoc (comm _ (of_env_temps _)) wand_elim_r.
+  - intros <-. apply wand_intro_l. by rewrite -(comm _ (of_env_temps _)) assoc.
+Qed.
+
+Lemma tac_delay_destruct Δ Q i :
+  match envs_lookup_delete true i Δ with
+  | Some (p,P,Δ') => envs_entails_delayed Δ' [] [ETemp p P] Q
+  | None => False
+  end →
+  envs_entails Δ Q.
+Proof.
+  destruct (envs_lookup_delete true i Δ) as [[[p P] Δ']|] eqn:?; last done.
+  rewrite envs_entails_delayed_unfold envs_entails_eq /= => <-.
+  rewrite envs_lookup_delete_sound //. by rewrite right_id left_id comm.
+Qed.
+
+Lemma tac_force Δ acts Q :
+  match envs_actions_app acts Δ with
+  | Some Δ' => envs_entails Δ' Q
+  | None => False
+  end →
+  envs_entails_delayed Δ acts [] Q.
+Proof.
+  destruct (envs_actions_app acts Δ) as [Δ'|] eqn:?; last done.
+  rewrite envs_entails_delayed_unfold envs_entails_eq /= => <-.
+  by rewrite left_id comm envs_actions_app_sound.
+Qed.
+
+Lemma tac_delayed_rename Δ acts tmps (p : bool) mi P Q :
+  envs_entails_delayed Δ (EAction p mi P :: acts) tmps Q →
+  envs_entails_delayed Δ acts (ETemp p P :: tmps) Q.
+Proof. rewrite !envs_entails_delayed_unfold /= => <-. solve_sep_entails. Qed.
+
+Lemma tac_delayed_falso Δ acts tmps p P Q :
+  FromAssumption p P False →
+  envs_entails_delayed Δ acts (ETemp p P :: tmps) Q.
+Proof.
+  rewrite !envs_entails_delayed_unfold /= => ->.
+  rewrite !left_absorb. apply False_elim.
+Qed.
+
+Lemma tac_delayed_clear Δ acts tmps (p : bool) P Q :
+  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) →
+  envs_entails_delayed Δ acts tmps Q →
+  envs_entails_delayed Δ acts (ETemp p P :: tmps) Q.
+Proof.
+  rewrite !envs_entails_delayed_unfold /= => HPQ HQ.
+  rewrite -!assoc HQ. destruct p; simpl; by rewrite sep_elim_r.
+Qed.
+Lemma tac_delayed_pure Δ acts tmps (p : bool) P Q φ :
+  IntoPure P φ →
+  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) →
+  (φ → envs_entails_delayed Δ acts tmps Q) →
+  envs_entails_delayed Δ acts (ETemp p P :: tmps) Q.
+Proof.
+  rewrite !envs_entails_delayed_unfold /= => ? HPQ HQ. rewrite -!assoc.
+  destruct p; simpl.
+  { rewrite (into_pure P) intuitionistically_affinely -persistent_and_affinely_sep_l.
+    auto using pure_elim_l. }
+  destruct HPQ.
+  - rewrite -(affine_affinely P) (into_pure P) -persistent_and_affinely_sep_l.
+    auto using pure_elim_l.
+  - rewrite (into_pure P) (persistent_absorbingly_affinely_2 ⌜ _ ⌝)%I.
+    rewrite !absorbingly_sep_l -(absorbing_absorbingly Q); f_equiv.
+    rewrite -persistent_and_affinely_sep_l. auto using pure_elim_l.
+Qed.
+
+Lemma tac_delayed_and Δ acts tmps (p : bool) P P1 P2 Q :
+  (if p then IntoAnd true P P1 P2 else IntoSep P P1 P2) →
+  envs_entails_delayed Δ acts (ETemp p P1 :: ETemp p P2 :: tmps) Q →
+  envs_entails_delayed Δ acts (ETemp p P :: tmps) Q.
+Proof.
+  rewrite !envs_entails_delayed_unfold /= -!assoc=> HP <-. destruct p.
+  - rewrite (into_and true P) /= .
+    by rewrite intuitionistically_and persistent_and_sep_1 -!assoc.
+  - by rewrite (into_sep P) /= -!assoc.
+Qed.
+
+Lemma tac_delayed_and_l Δ acts tmps (p : bool) P P1 P2 Q :
+  (if p then IntoAnd p P P1 P2 else
+   TCOr (IntoAnd p P P1 P2)
+        (TCAnd (IntoSep P P1 P2) (TCOr (Affine P2) (Absorbing Q)))) →
+  envs_entails_delayed Δ acts (ETemp p P1 :: tmps) Q →
+  envs_entails_delayed Δ acts (ETemp p P :: tmps) Q.
+Proof.
+  rewrite !envs_entails_delayed_unfold /= -!assoc=> HP HQ. destruct p.
+  { by rewrite (into_and true P) /= and_elim_l. }
+  destruct HP as [?|[? HP2Q]].
+  { by rewrite (into_and false P) /= and_elim_l. }
+  rewrite (into_sep P) /=. destruct HP2Q.
+  - by rewrite (sep_elim_l P1 P2).
+  - by rewrite (comm _ P1) -!assoc HQ sep_elim_r.
+Qed.
+Lemma tac_delayed_and_r Δ acts tmps (p : bool) P P1 P2 Q :
+  (if p then IntoAnd p P P1 P2 else
+   TCOr (IntoAnd p P P1 P2)
+        (TCAnd (IntoSep P P1 P2) (TCOr (Affine P1) (Absorbing Q)))) →
+  envs_entails_delayed Δ acts (ETemp p P2 :: tmps) Q →
+  envs_entails_delayed Δ acts (ETemp p P :: tmps) Q.
+Proof.
+  rewrite !envs_entails_delayed_unfold /= -!assoc=> HP HQ. destruct p.
+  { by rewrite (into_and true P) /= and_elim_r. }
+  destruct HP as [?|[? HP2Q]].
+  { by rewrite (into_and false P) /= and_elim_r. }
+  rewrite (into_sep P) /=. destruct HP2Q.
+  - by rewrite (sep_elim_r P1 P2).
+  - by rewrite -!assoc HQ sep_elim_r.
+Qed.
+
+Lemma tac_delayed_or Δ acts tmps (p : bool) P P1 P2 Q :
+  IntoOr P P1 P2 →
+  envs_entails_delayed Δ acts (ETemp p P1 :: tmps) Q →
+  envs_entails_delayed Δ acts (ETemp p P2 :: tmps) Q →
+  envs_entails_delayed Δ acts (ETemp p P :: tmps) Q.
+Proof.
+  rewrite !envs_entails_delayed_unfold /= -!assoc=> HP HQ1 HQ2.
+  rewrite (into_or P) intuitionistically_if_or sep_or_r. by apply or_elim.
+Qed.
+
+Lemma tac_delayed_intuitionistic Δ acts tmps (p : bool) P P' Q :
+  IntoPersistent p P P' →
+  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) →
+  envs_entails_delayed Δ acts (ETemp true P' :: tmps) Q →
+  envs_entails_delayed Δ acts (ETemp p P :: tmps) Q.
+Proof.
+  rewrite /IntoPersistent !envs_entails_delayed_unfold /= -!assoc=> HP HPQ HQ.
+  destruct p; simpl in *.
+  { by rewrite /bi_intuitionistically HP.  }
+  destruct HPQ.
+  - by rewrite -(affine_affinely P) HP.
+  - rewrite HP -absorbingly_intuitionistically_into_persistently.
+    by rewrite absorbingly_sep_l HQ.
+Qed.
+
+Lemma tac_delayed_modal Δ acts tmps p p' P P' Q Q' φ :
+  ElimModal φ p p' P P' Q Q' →
+  φ →
+  envs_entails_delayed Δ acts (ETemp p' P' :: tmps) Q' →
+  envs_entails_delayed Δ acts (ETemp p P :: tmps) Q.
+Proof.
+  rewrite /ElimModal !envs_entails_delayed_unfold /= -!assoc => HP Hφ HQ'.
+  rewrite -HP //. apply sep_mono; first done. by apply wand_intro_l.
+Qed.
+
+Lemma tac_delayed_frame Δ acts tmps p P Q Q' :
+  Frame p P Q Q' →
+  envs_entails_delayed Δ (if p then EAction p None P :: acts else acts) tmps Q' →
+  envs_entails_delayed Δ acts (ETemp p P :: tmps) Q.
+Proof.
+  rewrite /Frame !envs_entails_delayed_unfold /= -!assoc=> <- <-.
+  destruct p; simpl; last done.
+  rewrite {1}(intuitionistically_sep_dup P). solve_sep_entails.
+Qed.
 End bi_tactics.
 
 (** The following _private_ classes are used internally by [tac_modal_intro] /
diff --git a/theories/proofmode/environments.v b/theories/proofmode/environments.v
index 40b077ccd6eb3d4fa0181cf4af2375686e9b3a5b..ecc556800fccb5607d7e5c0a4d0182723f9c497e 100644
--- a/theories/proofmode/environments.v
+++ b/theories/proofmode/environments.v
@@ -373,6 +373,44 @@ Definition env_to_prop {PROP : bi} (Γ : env PROP) : PROP :=
   in
   match Γ with Enil => emp%I | Esnoc Γ _ P => aux Γ P end.
 
+Inductive env_temp (PROP : bi) :=
+  | ETemp (p : bool) (P : PROP).
+Arguments ETemp {_} _ _.
+Inductive env_action (PROP : bi) :=
+  | EAction (p : bool) (i : option ident) (P : PROP).
+Arguments EAction {_} _ _ _.
+
+Definition of_env_temp {PROP} (act : env_temp PROP) : PROP :=
+  match act with ETemp p P => â–¡?p P end%I.
+Definition of_env_action {PROP} (act : env_action PROP) : PROP :=
+  match act with EAction p _ P => â–¡?p P end%I.
+
+Definition envs_entails_delayed {PROP : bi} (Δ : envs PROP)
+    (acts : list (env_action PROP)) (tmps : list (env_temp PROP)) (Q : PROP) :=
+  envs_entails Δ (([∗ list] act ∈ acts, of_env_action act) ∗
+                  ([∗ list] tmp ∈ tmps, of_env_temp tmp) -∗ Q).
+
+Fixpoint envs_actions_flatten {PROP} (acts : list (env_action PROP))
+    (c : positive) (Γp Γs : env PROP) : (positive * env PROP * env PROP) :=
+  match acts with
+  | [] => (c,Γp,Γs)
+  | EAction q None P :: acts =>
+     if q
+     then envs_actions_flatten acts (Pos_succ c) (Esnoc Γp (IAnon c) P) Γs
+     else envs_actions_flatten acts (Pos_succ c) Γp (Esnoc Γs (IAnon c) P)
+  | EAction q (Some j) P :: acts =>
+     if q
+     then envs_actions_flatten acts c (Esnoc Γp j P) Γs
+     else envs_actions_flatten acts c Γp (Esnoc Γs j P)
+  end.
+
+Definition envs_actions_app {PROP}
+    (acts : list (env_action PROP)) (Δ : envs PROP) : option (envs PROP) :=
+  let '(c,Γp,Γs) := envs_actions_flatten (pm_reverse acts) (env_counter Δ) Enil Enil in
+  Δ ← envs_app true Γp Δ;
+  Δ ← envs_app false Γs Δ;
+  Some (envs_set_counter c Δ).
+
 Section envs.
 Context {PROP : bi}.
 Implicit Types Γ Γp Γs : env PROP.
@@ -777,4 +815,43 @@ Proof.
   - by rewrite right_id.
   - rewrite /= IH (comm _ Q _) assoc. done.
 Qed.
+
+Lemma envs_replace_action_filter_sound acts c Γp Γs c' Γp' Γs' :
+  envs_actions_flatten acts c Γp Γs = (c',Γp',Γs') →
+  ([∗ list] act ∈ acts, of_env_action act) ∗ □ [∧] Γp ∗ [∗] Γs
+  ⊢ □ [∧] Γp' ∗ [∗] Γs'.
+Proof.
+  revert c Γp Γs.
+  induction acts as [|[q [j|] P] acts IH]=> c Γp Γs ?; simplify_eq/=.
+  - by rewrite left_id.
+  - destruct q; simplify_eq/=.
+    + rewrite -IH //; simpl.
+      rewrite intuitionistically_and and_sep_intuitionistically. solve_sep_entails.
+    + rewrite -IH //; simpl. solve_sep_entails.
+  - destruct q; simplify_eq/=.
+    + rewrite -IH //; simpl.
+      rewrite intuitionistically_and and_sep_intuitionistically. solve_sep_entails.
+    + rewrite -IH //; simpl. solve_sep_entails.
+Qed.
+
+Lemma envs_replace_action_filter_sound_nil acts c c' Γp' Γs' :
+  envs_actions_flatten acts c Enil Enil = (c',Γp',Γs') →
+  ([∗ list] act ∈ acts, of_env_action act) ⊢ □ [∧] Γp' ∗ [∗] Γs'.
+Proof.
+  intros. rewrite -envs_replace_action_filter_sound //; simpl.
+  by rewrite intuitionistically_True_emp !right_id.
+Qed.
+
+Lemma envs_actions_app_sound Δ Δ' acts :
+  envs_actions_app acts Δ = Some Δ' →
+  of_envs Δ ∗ ([∗ list] act ∈ acts, of_env_action act) ⊢ of_envs Δ'.
+Proof.
+  rewrite /envs_actions_app=> Hacts.
+  destruct (envs_actions_flatten _ _ _ _) as [[c Γp] Γs] eqn:?.
+  destruct (envs_app true _ _) as [Δ1|] eqn:?; simplify_eq/=.
+  destruct (envs_app false _ _) as [Δ2|] eqn:?; simplify_eq/=.
+  rewrite envs_app_sound // envs_app_sound // envs_set_counter_sound; simpl.
+  rewrite -(reverse_Permutation acts) envs_replace_action_filter_sound_nil //.
+  by rewrite wand_curry wand_elim_l.
+Qed.
 End envs.
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index b349b89140ead7624471ec63e6ff9efa17cb5c28..ec40edd623d644de014e24babc8650218734e360 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -1288,29 +1288,128 @@ Tactic Notation "iModCore" constr(H) :=
     |pm_reduce; pm_prettify(* subgoal *)].
 
 (** * Basic destruct tactic *)
-Local Ltac iDestructHypGo Hz pat :=
+Local Ltac iFastDestructHypGo pat :=
   lazymatch pat with
   | IFresh =>
-     lazymatch Hz with
-     | IAnon _ => idtac
-     | INamed ?Hz => let Hz' := iFresh in iRename Hz into Hz'
-     end
-  | IDrop => iClearHyp Hz
-  | IFrame => iFrameHyp Hz
-  | IIdent ?y => iRename Hz into y
-  | IList [[]] => iExFalso; iExact Hz
-  | IList [[?pat1; IDrop]] => iAndDestructChoice Hz as Left Hz; iDestructHypGo Hz pat1
-  | IList [[IDrop; ?pat2]] => iAndDestructChoice Hz as Right Hz; iDestructHypGo Hz pat2
+     eapply (tac_delayed_rename _ _ _ _ None)
+  | IIdent ?y =>
+     eapply (tac_delayed_rename _ _ _ _ (Some y))
+  | IDrop =>
+     eapply tac_delayed_clear;
+       [pm_reduce; iSolveTC ||
+        let P := match goal with |- TCOr (Affine ?P) _ => P end in
+        fail "iDestruct: cannot clear" P "; not affine and the goal not absorbing"
+       |]
+  | IFrame =>
+     eapply tac_delayed_frame;
+       [iSolveTC ||
+        let R := match goal with |- Frame _ ?R _ _ => R end in
+        fail "iDestruct: cannot frame" R
+       |]
+  | IList [[]] =>
+     eapply tac_delayed_falso;
+       [iSolveTC ||
+        let P := match goal with |- FromAssumption _ ?P _ => P end in
+        fail "iDestruct:" P " is not False"]
+  | IList [[?pat; IDrop]] =>
+     eapply tac_delayed_and_l;
+       [pm_reduce; iSolveTC ||
+        let P := match goal with |- context [ IntoAnd _ ?P _ _ ] => P end in
+        fail "iDestruct: cannot destruct" P
+       |iFastDestructHypGo pat]
+  | IList [[IDrop; ?pat]] =>
+     eapply tac_delayed_and_r;
+       [pm_reduce; iSolveTC ||
+        let P := match goal with |- context [ IntoAnd _ ?P _ _ ] => P end in
+        fail "iDestruct: cannot destruct" P
+       |iFastDestructHypGo pat]
   | IList [[?pat1; ?pat2]] =>
-     let Hy := iFresh in iAndDestruct Hz as Hz Hy; iDestructHypGo Hz pat1; iDestructHypGo Hy pat2
-  | IList [[?pat1];[?pat2]] => iOrDestruct Hz as Hz Hz; [iDestructHypGo Hz pat1|iDestructHypGo Hz pat2]
-  | IPureElim => iPure Hz as ?
-  | IRewrite Right => iPure Hz as ->
-  | IRewrite Left => iPure Hz as <-
-  | IAlwaysElim ?pat => iIntuitionistic Hz; iDestructHypGo Hz pat
-  | IModalElim ?pat => iModCore Hz; iDestructHypGo Hz pat
+     eapply tac_delayed_and;
+       [pm_reduce; iSolveTC ||
+        let P :=
+          lazymatch goal with
+          | |- IntoSep ?P _ _ => P
+          | |- IntoAnd _ ?P _ _ => P
+          end in
+        fail "iDestruct: cannot destruct" P
+       |iFastDestructHypGo pat1; iFastDestructHypGo pat2]
+  | IList [[?pat1];[?pat2]] =>
+     eapply tac_delayed_or;
+       [pm_reduce; iSolveTC ||
+        let P := match goal with |- context [ IntoOr ?P _ _ ] => P end in
+        fail "iDestruct: cannot turn " P "into a disjunction"
+       |iFastDestructHypGo pat1
+       |iFastDestructHypGo pat2]
+  | IPureElim =>
+     eapply tac_delayed_pure;
+       [iSolveTC ||
+        let P := match goal with |- IntoPure ?P _ => P end in
+        fail "iDestruct:" P "not pure"
+       |pm_reduce; iSolveTC ||
+        let P := match goal with |- TCOr (Affine ?P) _ => P end in
+        fail "iDestruct:" P "not affine and the goal not absorbing"
+       |intros ?]
+  | IRewrite Right =>
+     (* Get rid of the duplication *)
+     eapply tac_delayed_pure;
+       [iSolveTC ||
+        let P := match goal with |- IntoPure ?P _ => P end in
+        fail "iDestruct:" P "not pure"
+       |pm_reduce; iSolveTC ||
+        let P := match goal with |- TCOr (Affine ?P) _ => P end in
+        fail "iDestruct:" P "not affine and the goal not absorbing"
+       |intros ->]
+  | IRewrite Left =>
+     (* Get rid of the duplication *)
+     eapply tac_delayed_pure;
+       [iSolveTC ||
+        let P := match goal with |- IntoPure ?P _ => P end in
+        fail "iDestruct:" P "not pure"
+       |pm_reduce; iSolveTC ||
+        let P := match goal with |- TCOr (Affine ?P) _ => P end in
+        fail "iDestruct:" P "not affine and the goal not absorbing"
+       |intros <-]
+  | IAlwaysElim ?pat =>
+     eapply tac_delayed_intuitionistic;
+       [iSolveTC ||
+        let P := match goal with |- IntoPersistent _ ?P _ => P end in
+        fail "iDestruct:" P "not persistent"
+       |pm_reduce; iSolveTC ||
+        let P := match goal with |- TCOr (Affine ?P) _ => P end in
+        fail "iDestruct:" P "not affine and the goal not absorbing"
+       |iFastDestructHypGo pat]
+  | IModalElim ?pat =>
+     eapply tac_delayed_modal;
+       [iSolveTC ||
+        let P := match goal with |- ElimModal _ _ _ ?P _ _ _ => P end in
+        let Q := match goal with |- ElimModal _ _ _ _ _ ?Q _ => Q end in
+        fail "iMod: cannot eliminate modality" P "in" Q
+       |iSolveSideCondition
+       |iFastDestructHypGo pat]
   | _ => fail "iDestruct:" pat "invalid"
   end.
+
+Tactic Notation "iFastDestructHyp" constr(H) "as" constr(pat) :=
+  let pat := intro_pat.parse_one pat in
+  iStartProof;
+  notypeclasses refine (tac_delay_destruct _ _ H _);
+  pm_reduce;
+  lazymatch goal with
+  | |- False => fail "iDestruct:" H "not found"
+  | |- envs_entails_delayed ?Δ ?acts ?tmps ?Q =>
+     let HΔ := fresh "Δ" in
+     pose (HΔ := Δ);
+     convert_concl_no_check (envs_entails_delayed HΔ acts tmps Q);
+     iFastDestructHypGo pat;
+     notypeclasses refine (tac_force _ _ _ _);
+     unfold HΔ; clear HΔ;
+     pm_reduce;
+     lazymatch goal with
+     | |- False => fail "iDestruct: given names not fresh"
+     | |- _ => idtac
+     end
+  end.
+
 Local Ltac iDestructHypFindPat Hgo pat found pats :=
   lazymatch pats with
   | [] =>
@@ -1323,7 +1422,7 @@ Local Ltac iDestructHypFindPat Hgo pat found pats :=
   | IClearFrame ?H :: ?pats => iFrame H; iDestructHypFindPat Hgo pat found pats
   | ?pat :: ?pats =>
      lazymatch found with
-     | false => iDestructHypGo Hgo pat; iDestructHypFindPat Hgo pat true pats
+     | false => iFastDestructHyp Hgo as pat; iDestructHypFindPat Hgo pat true pats
      | true => fail "iDestruct:" pat "should contain exactly one proper introduction pattern"
      end
   end.
diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index 0c9e1e9f3bbb59971b42981cbfe7bd05836d4414..578b99923925bad2bfe5c4a80f93a86fb2b9af90 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -192,7 +192,7 @@ Global Instance as_emp_valid_monPred_at_equiv φ P Q (Φ Ψ : I → PROP) :
 Proof.
   rewrite /AsEmpValid0 /AsEmpValid /MakeMonPredAt. intros -> EQ1 EQ2.
   setoid_rewrite <-EQ1. setoid_rewrite <-EQ2. split.
-  - move=>/bi.wand_iff_equiv HP. setoid_rewrite HP. iIntros. iSplit; iIntros "$".
+  - move=>/bi.wand_iff_equiv HP. setoid_rewrite HP. iIntros. iSplit; by iIntros "$".
   - move=>HP. apply bi.equiv_wand_iff. split=>i. by iSplit; iIntros; iApply HP.
 Qed.
 
diff --git a/theories/proofmode/reduction.v b/theories/proofmode/reduction.v
index 4b1c225d4bc2cc3d955fe6b47a8cccd879f57792..cae8af01ddf56dab9d409f45d1b5d9e2b80e80b8 100644
--- a/theories/proofmode/reduction.v
+++ b/theories/proofmode/reduction.v
@@ -14,6 +14,7 @@ Declare Reduction pm_eval := cbv [
   envs_simple_replace envs_replace envs_split
   envs_clear_spatial envs_clear_intuitionistic envs_set_counter envs_incr_counter
   envs_split_go envs_split env_to_prop
+  envs_actions_flatten envs_actions_app
   (* PM list and option combinators *)
   pm_app pm_rev_append pm_reverse pm_foldr pm_list_fmap pm_list_bind pm_list_mapM
   pm_option_bind pm_from_option pm_option_fun