diff --git a/_CoqProject b/_CoqProject
index f404e380b28d1252318172a1e61e37b703c5acb1..92fc6bd868e7653ba9dcbda026a271ce755ef9f5 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -39,6 +39,7 @@ theories/bi/tactics.v
 theories/bi/monpred.v
 theories/bi/embedding.v
 theories/bi/weakestpre.v
+theories/bi/telescopes.v
 theories/bi/lib/counter_examples.v
 theories/bi/lib/fixpoint.v
 theories/bi/lib/fractional.v
diff --git a/tests/ipm_paper.ref b/tests/ipm_paper.ref
index 315580437da3ebf0ac765131930c17bbb43cdc76..9bcb74f82069801b5c48be7eae96fc66eb070ff9 100644
--- a/tests/ipm_paper.ref
+++ b/tests/ipm_paper.ref
@@ -1,3 +1,5 @@
+"sep_exist"
+     : string
 1 subgoal
   
   M : ucmraT
@@ -44,6 +46,8 @@ P
   --------------------------------------∗
   P
   
+"sep_exist_short"
+     : string
 1 subgoal
   
   M : ucmraT
@@ -57,6 +61,8 @@ P
   --------------------------------------∗
   ∃ a : A, Ψ a ∗ P
   
+"read_spec"
+     : string
 1 subgoal
   
   Σ : gFunctors
diff --git a/tests/ipm_paper.v b/tests/ipm_paper.v
index f423ed2138e07bf0d65ea1c797cfebf78c5c19fd..179183d14cd686bbed77dae492e17c53db0b7c40 100644
--- a/tests/ipm_paper.v
+++ b/tests/ipm_paper.v
@@ -25,6 +25,7 @@ Section demo.
   Qed.
 
   (* The version in IPM *)
+  Check "sep_exist".
   Lemma sep_exist A (P R: iProp) (Ψ: A → iProp) :
     P ∗ (∃ a, Ψ a) ∗ R ⊢ ∃ a, Ψ a ∗ P.
   Proof.
@@ -35,6 +36,7 @@ Section demo.
   Qed.
 
   (* The short version in IPM, as in the paper *)
+  Check "sep_exist_short".
   Lemma sep_exist_short A (P R: iProp) (Ψ: A → iProp) :
     P ∗ (∃ a, Ψ a) ∗ R ⊢ ∃ a, Ψ a ∗ P.
   Proof. iIntros "[HP [HΨ HR]]". Show. iFrame "HP". iAssumption. Qed.
@@ -235,6 +237,7 @@ Section counter_proof.
       wp_if. iApply ("IH" with "[Hγf]"). rewrite {3}/C; eauto 10.
   Qed.
 
+  Check "read_spec".
   Lemma read_spec l n :
     {{ C l n }} read #l {{ v, ∃ m : nat, ⌜v = #m ∧ n ≤ m⌝ ∧ C l m }}.
   Proof.
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 34c19e80bffec54123e56fab3628de71f9514b7d..d9611c679930d143cd554bb15ade01740e6deea6 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -59,6 +59,31 @@ In nested Ltac calls to "iSpecialize (open_constr)",
 "iSpecializePat (open_constr) (constr)" and "iSpecializePat_go", last call
 failed.
 Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I with P.
+1 subgoal
+  
+  PROP : sbi
+  P, Q : PROP
+  n, m, k : nat
+  ============================
+  --------------------------------------∗
+  â–·^(S n + S m) emp
+  
+1 subgoal
+  
+  PROP : sbi
+  P, Q : PROP
+  ============================
+  --------------------------------------∗
+  â–· emp
+  
+1 subgoal
+  
+  PROP : sbi
+  P, Q : PROP
+  ============================
+  --------------------------------------∗
+  â–· emp
+  
 The command has indeed failed with message:
 In nested Ltac calls to "iFrame (constr)",
 "<iris.proofmode.ltac_tactics.iFrame_go>" and
@@ -114,6 +139,52 @@ Tactic failure: iFrame: cannot frame Q.
   --------------------------------------∗
   <absorb> Φ x1 x2
   
+1 subgoal
+  
+  PROP : sbi
+  ============================
+  "H" : â–¡ True
+  --------------------------------------∗
+  True
+  
+1 subgoal
+  
+  PROP : sbi
+  ============================
+  "H" : emp
+  --------------------------------------â–¡
+  â–¡ emp
+  
+1 subgoal
+  
+  PROP : sbi
+  ============================
+  "H" : emp
+  --------------------------------------â–¡
+  â–¡ emp
+  
+1 subgoal
+  
+  PROP : sbi
+  mP : option PROP
+  Q, R : PROP
+  ============================
+  "HPQ" : mP -∗? Q
+  "HQR" : Q -∗ R
+  "HP" : pm_default emp mP
+  --------------------------------------∗
+  R
+  
+1 subgoal
+  
+  PROP : sbi
+  mP : option PROP
+  Q, R : PROP
+  ============================
+  "HP" : pm_default emp mP
+  --------------------------------------∗
+  pm_default emp mP
+  
 1 subgoal
   
   PROP : sbi
diff --git a/tests/proofmode.v b/tests/proofmode.v
index dc0a4641706e163ffb75f81698045e5b6f57c09e..48d83b752233a4de1f353cdfbb5c086a0e3d86c4 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -367,7 +367,7 @@ Lemma test_iNext_plus_2 P n m : ▷^n ▷^m P -∗ ▷^(n+m) P.
 Proof. iIntros "H". iNext. done. Qed.
 Lemma test_iNext_plus_3 P Q n m k :
   ▷^m ▷^(2 + S n + k) P -∗ ▷^m ▷ ▷^(2 + S n) Q -∗ ▷^k ▷ ▷^(S (S n + S m)) (P ∗ Q).
-Proof. iIntros "H1 H2". iNext. iNext. iNext. iFrame. Qed.
+Proof. iIntros "H1 H2". iNext. iNext. iNext. iFrame. Show. iModIntro. done. Qed.
 
 Lemma test_iNext_unfold P Q n m (R := (â–·^n P)%I) :
   R ⊢ ▷^m True.
@@ -409,10 +409,10 @@ Lemma test_iPureIntro_absorbing (φ : Prop) :
 Proof. intros ?. iPureIntro. done. Qed.
 
 Lemma test_iFrame_later_1 P Q : P ∗ ▷ Q -∗ ▷ (P ∗ ▷ Q).
-Proof. iIntros "H". iFrame "H". auto. Qed.
+Proof. iIntros "H". iFrame "H". Show. auto. Qed.
 
 Lemma test_iFrame_later_2 P Q : ▷ P ∗ ▷ Q -∗ ▷ (▷ P ∗ ▷ Q).
-Proof. iIntros "H". iFrame "H". auto. Qed.
+Proof. iIntros "H". iFrame "H". Show. auto. Qed.
 
 Lemma test_with_ident P Q R : P -∗ Q -∗ (P -∗ Q -∗ R) -∗ R.
 Proof.
@@ -490,7 +490,7 @@ Lemma test_big_sepL_simpl x (l : list nat) P :
   ([∗ list] k↦y ∈ l, <affine> ⌜ y = y ⌝) -∗
   ([∗ list] y ∈ x :: l, <affine> ⌜ y = y ⌝) -∗
   P.
-Proof. iIntros "HP ?? /=". Show. done. Qed.
+Proof. iIntros "HP ??". Show. done. Qed.
 
 Lemma test_big_sepL2_simpl x1 x2 (l1 l2 : list nat) P :
   P -∗
@@ -508,6 +508,42 @@ Lemma test_big_sepL2_iFrame (Φ : nat → nat → PROP) (l1 l2 : list nat) P :
   Φ 0 10 -∗ ([∗ list] y1;y2 ∈ l1;l2, Φ y1 y2) -∗
   ([∗ list] y1;y2 ∈ (0 :: l1);(10 :: l2), Φ y1 y2).
 Proof. iIntros "$ ?". iFrame. Qed.
+
+Lemma test_lemma_1 (b : bool) :
+  emp ⊢@{PROP} □?b True.
+Proof. destruct b; simpl; eauto. Qed.
+Lemma test_reducing_after_iDestruct : emp ⊢@{PROP} True.
+Proof.
+  iIntros "H". iDestruct (test_lemma_1 true with "H") as "H". Show. done.
+Qed.
+
+Lemma test_lemma_2 (b : bool) :
+  □?b emp ⊢@{PROP} emp.
+Proof. destruct b; simpl; eauto. Qed.
+Lemma test_reducing_after_iApply : emp ⊢@{PROP} emp.
+Proof.
+  iIntros "#H". iApply (test_lemma_2 true). Show. auto.
+Qed.
+
+Lemma test_lemma_3 (b : bool) :
+  □?b emp ⊢@{PROP} ⌜b = b⌝.
+Proof. destruct b; simpl; eauto. Qed.
+Lemma test_reducing_after_iApply_late_evar : emp ⊢@{PROP} ⌜true = true⌝.
+Proof.
+  iIntros "#H". iApply (test_lemma_3). Show. auto.
+Qed.
+
+Section wandM.
+  Import proofmode.base.
+  Lemma test_wandM mP Q R :
+    (mP -∗? Q) -∗ (Q -∗ R) -∗ (mP -∗? R).
+  Proof.
+    iIntros "HPQ HQR HP". Show.
+    iApply "HQR". iApply "HPQ". Show.
+    done.
+  Qed.
+End wandM.
+
 End tests.
 
 (** Test specifically if certain things print correctly. *)
diff --git a/tests/telescopes.ref b/tests/telescopes.ref
new file mode 100644
index 0000000000000000000000000000000000000000..0816c1fa580fdb2ee3576d27ddb20c1fdef07ef4
--- /dev/null
+++ b/tests/telescopes.ref
@@ -0,0 +1,93 @@
+1 subgoal
+  
+  PROP : sbi
+  BiFUpd0 : BiFUpd PROP
+  X : tele
+  E1, E2 : coPset
+  α, β, γ1, γ2 : X → PROP
+  x' : X
+  ============================
+  "Hγ12" : ∀.. x : X, γ1 x -∗ γ2 x
+  "Hα" : α x'
+  "Hclose" : β x' ={E2,E1}=∗ γ1 x'
+  --------------------------------------∗
+  |={E2}=> ∃.. x : X, α x ∗ (β x ={E2,E1}=∗ γ2 x)
+  
+1 subgoal
+  
+  PROP : sbi
+  BiFUpd0 : BiFUpd PROP
+  E1, E2 : coPset
+  ============================
+  "H" : ∃ x x0 : nat, <affine> ⌜x = x0⌝ ∗ (True ={E2,E1}=∗ <affine> ⌜x ≠ x0⌝)
+  --------------------------------------∗
+  |={E2,E1}=> False
+  
+"test1_test"
+     : string
+1 subgoal
+  
+  PROP : sbi
+  x : nat
+  ============================
+  "H" : ∃ x0 : nat, <affine> ⌜x = x0⌝
+  --------------------------------------∗
+  â–· False
+  
+1 subgoal
+  
+  PROP : sbi
+  x : nat
+  ============================
+  "H" : ∃ x0 : nat, <affine> ⌜x = x0⌝
+  --------------------------------------∗
+  â–· False
+  
+"test2_test"
+     : string
+1 subgoal
+  
+  PROP : sbi
+  ============================
+  "H" : ∃ x x0 : nat, <affine> ⌜x = x0⌝
+  --------------------------------------∗
+  False
+  
+1 subgoal
+  
+  PROP : sbi
+  x : nat
+  ============================
+  "H" : ∃ x0 : nat, <affine> ⌜x = x0⌝
+  --------------------------------------∗
+  False
+  
+1 subgoal
+  
+  PROP : sbi
+  x : nat
+  ============================
+  "H" : ▷ (∃ x0 : nat, <affine> ⌜x = x0⌝)
+  --------------------------------------∗
+  â–· False
+  
+"test3_test"
+     : string
+1 subgoal
+  
+  PROP : sbi
+  x : nat
+  ============================
+  "H" : ∃ x0 : nat, <affine> ⌜x = x0⌝
+  --------------------------------------∗
+  â–· False
+  
+1 subgoal
+  
+  PROP : sbi
+  x : nat
+  ============================
+  "H" : ◇ (∃ x0 : nat, <affine> ⌜x = x0⌝)
+  --------------------------------------∗
+  â–· False
+  
diff --git a/tests/telescopes.v b/tests/telescopes.v
new file mode 100644
index 0000000000000000000000000000000000000000..621e086dff47bb7aed49c11191c4f511fe1ad9fd
--- /dev/null
+++ b/tests/telescopes.v
@@ -0,0 +1,113 @@
+From stdpp Require Import coPset namespaces.
+From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type".
+
+Section accessor.
+(* Just playing around a bit with a telescope version
+   of accessors with just one binder list. *)
+Definition accessor `{!BiFUpd PROP} {X : tele} (E1 E2 : coPset)
+           (α β γ : X → PROP) : PROP :=
+  (|={E1,E2}=> ∃.. x, α x ∗ (β x -∗ |={E2,E1}=> (γ x)))%I.
+
+Notation "'ACC' @ E1 , E2 {{ ∃ x1 .. xn , α | β | γ } }" :=
+  (accessor (X:=TeleS (fun x1 => .. (TeleS (fun xn => TeleO)) .. ))
+            E1 E2
+            (tele_app (TT:=TeleS (fun x1 => .. (TeleS (fun xn => TeleO)) .. )) $
+                      fun x1 => .. (fun xn => α%I) ..)
+            (tele_app (TT:=TeleS (fun x1 => .. (TeleS (fun xn => TeleO)) .. )) $
+                      fun x1 => .. (fun xn => β%I) ..)
+            (tele_app (TT:=TeleS (fun x1 => .. (TeleS (fun xn => TeleO)) .. )) $
+                      fun x1 => .. (fun xn => γ%I) ..))
+  (at level 20, α, β, γ at level 200, x1 binder, xn binder, only parsing).
+
+(* Working with abstract telescopes. *)
+Section tests.
+Context `{!BiFUpd PROP} {X : tele}.
+Implicit Types α β γ : X → PROP.
+
+Lemma acc_mono E1 E2 α β γ1 γ2 :
+  (∀.. x, γ1 x -∗ γ2 x) -∗
+  accessor E1 E2 α β γ1 -∗ accessor E1 E2 α β γ2.
+Proof.
+  iIntros "Hγ12 >Hacc". iDestruct "Hacc" as (x') "[Hα Hclose]". Show.
+  iModIntro. iExists x'. iFrame. iIntros "Hβ".
+  iMod ("Hclose" with "Hβ") as "Hγ". iApply "Hγ12". auto.
+Qed.
+End tests.
+
+Section printing_tests.
+Context `{!BiFUpd PROP}.
+
+(* Working with concrete telescopes: Testing the reduction into normal quantifiers. *)
+Lemma acc_elim_test_1 E1 E2 :
+  ACC @ E1, E2 {{ ∃ a b : nat, <affine> ⌜a = b⌝ | True | <affine> ⌜a ≠ b⌝ }}
+    ⊢@{PROP} |={E1}=> False.
+Proof.
+  iIntros ">H". Show.
+  iDestruct "H" as (a b) "[% Hclose]". iMod ("Hclose" with "[//]") as "%".
+  done.
+Qed.
+End printing_tests.
+End accessor.
+
+(* Robbert's tests *)
+Section telescopes_and_tactics.
+
+Definition test1 {PROP : sbi} {X : tele} (α : X → PROP) : PROP :=
+  (∃.. x, α x)%I.
+
+Notation "'TEST1' {{ ∃ x1 .. xn , α } }" :=
+  (test1 (X:=TeleS (fun x1 => .. (TeleS (fun xn => TeleO)) .. ))
+            (tele_app (TT:=TeleS (fun x1 => .. (TeleS (fun xn => TeleO)) .. )) $
+                      fun x1 => .. (fun xn => α%I) ..))
+  (at level 20, α at level 200, x1 binder, xn binder, only parsing).
+
+Definition test2 {PROP : sbi} {X : tele} (α : X → PROP) : PROP :=
+  (▷ ∃.. x, α x)%I.
+
+Notation "'TEST2' {{ ∃ x1 .. xn , α } }" :=
+  (test2 (X:=TeleS (fun x1 => .. (TeleS (fun xn => TeleO)) .. ))
+            (tele_app (TT:=TeleS (fun x1 => .. (TeleS (fun xn => TeleO)) .. )) $
+                      fun x1 => .. (fun xn => α%I) ..))
+  (at level 20, α at level 200, x1 binder, xn binder, only parsing).
+
+Definition test3 {PROP : sbi} {X : tele} (α : X → PROP) : PROP :=
+  (◇ ∃.. x, α x)%I.
+
+Notation "'TEST3' {{ ∃ x1 .. xn , α } }" :=
+  (test3 (X:=TeleS (fun x1 => .. (TeleS (fun xn => TeleO)) .. ))
+            (tele_app (TT:=TeleS (fun x1 => .. (TeleS (fun xn => TeleO)) .. )) $
+                      fun x1 => .. (fun xn => α%I) ..))
+  (at level 20, α at level 200, x1 binder, xn binder, only parsing).
+
+Check "test1_test".
+Lemma test1_test {PROP : sbi}  :
+  TEST1 {{ ∃ a b : nat, <affine> ⌜a = b⌝ }} ⊢@{PROP} ▷ False.
+Proof.
+  iIntros "H". iDestruct "H" as (x) "H". Show.
+Restart.
+  iIntros "H". unfold test1. iDestruct "H" as (x) "H". Show.
+Abort.
+
+Check "test2_test".
+Lemma test2_test {PROP : sbi}  :
+  TEST2 {{ ∃ a b : nat, <affine> ⌜a = b⌝ }} ⊢@{PROP} ▷ False.
+Proof.
+  iIntros "H". iModIntro. Show.
+  iDestruct "H" as (x) "H". Show.
+Restart.
+  iIntros "H". iDestruct "H" as (x) "H". Show.
+Abort.
+
+Check "test3_test".
+Lemma test3_test {PROP : sbi}  :
+  TEST3 {{ ∃ a b : nat, <affine> ⌜a = b⌝ }} ⊢@{PROP} ▷ False.
+Proof.
+  iIntros "H". iMod "H".
+  iDestruct "H" as (x) "H".
+  Show.
+Restart.
+  iIntros "H". iDestruct "H" as (x) "H". Show.
+Abort.
+
+End telescopes_and_tactics.
diff --git a/theories/base_logic/bi.v b/theories/base_logic/bi.v
index 1b7fdb09dd1713dc4c55bbb7390d58783e760de7..114d50904479e1fcef0359cf5962830cccd94887 100644
--- a/theories/base_logic/bi.v
+++ b/theories/base_logic/bi.v
@@ -206,7 +206,7 @@ Lemma ofe_fun_validI `{B : A → ucmraT} (g : ofe_fun B) : ✓ g ⊣⊢ ∀ i, 
 Proof. exact: uPred_primitive.ofe_fun_validI. Qed.
 
 (** Consistency/soundness statement *)
-Lemma soundness φ n : (▷^n ⌜ φ ⌝ : uPred M)%I → φ.
+Lemma soundness_iter φ n : Nat.iter n sbi_later (⌜ φ ⌝ : uPred M)%I → φ.
 Proof. exact: uPred_primitive.soundness. Qed.
 
 End restate.
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 8ea72840f1c1e62ec2aab270564fca39b25b64e5..d3ff12d81d6622b48e7e5a107fbfd1e62512dab8 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -91,8 +91,10 @@ Global Instance uPred_ownM_sep_homomorphism :
   MonoidHomomorphism op uPred_sep (≡) (@uPred_ownM M).
 Proof. split; [split; try apply _|]. apply ownM_op. apply ownM_unit'. Qed.
 
-
 (** Consistency/soundness statement *)
+Lemma soundness φ n : (▷^n ⌜ φ ⌝ : uPred M)%I → φ.
+Proof. rewrite laterN_iter. apply soundness_iter. Qed.
+
 Corollary consistency_modal n : ¬ (▷^n False : uPred M)%I.
 Proof. exact (soundness False n). Qed.
 
diff --git a/theories/bi/derived_connectives.v b/theories/bi/derived_connectives.v
index 6cfef117eaa8da5d775c4c0dd27e382240238ff5..b6128cb5a1a52c783be801496f9065b13855dcd9 100644
--- a/theories/bi/derived_connectives.v
+++ b/theories/bi/derived_connectives.v
@@ -88,8 +88,11 @@ Fixpoint bi_hforall {PROP : bi} {As} : himpl As PROP → PROP :=
   | tcons A As => λ Φ, ∀ x, bi_hforall (Φ x)
   end%I.
 
-Definition sbi_laterN {PROP : sbi} (n : nat) (P : PROP) : PROP :=
-  Nat.iter n sbi_later P.
+Fixpoint sbi_laterN {PROP : sbi} (n : nat) (P : PROP) : PROP :=
+  match n with
+  | O => P
+  | S n' => â–· sbi_laterN n' P
+  end%I.
 Arguments sbi_laterN {_} !_%nat_scope _%I.
 Instance: Params (@sbi_laterN) 2.
 Notation "â–·^ n P" := (sbi_laterN n P) : bi_scope.
@@ -106,3 +109,15 @@ Arguments Timeless {_} _%I : simpl never.
 Arguments timeless {_} _%I {_}.
 Hint Mode Timeless + ! : typeclass_instances.
 Instance: Params (@Timeless) 1.
+
+(** An optional precondition [mP] to [Q].
+    TODO: We may actually consider generalizing this to a list of preconditions,
+    and e.g. also using it for texan triples. *)
+Definition bi_wandM {PROP : bi} (mP : option PROP) (Q : PROP) : PROP :=
+  match mP with
+  | None => Q
+  | Some P => (P -∗ Q)%I
+  end.
+Arguments bi_wandM {_} !_%I _%I /.
+Notation "mP -∗? Q" := (bi_wandM mP Q)
+  (at level 99, Q at level 200, right associativity) : bi_scope.
diff --git a/theories/bi/derived_laws_bi.v b/theories/bi/derived_laws_bi.v
index 14fe0f231b38add391652716114c7bd5567fed0b..b78d0fe7e99f1ee9e76a822b2a7e5452a7ab893d 100644
--- a/theories/bi/derived_laws_bi.v
+++ b/theories/bi/derived_laws_bi.v
@@ -460,6 +460,10 @@ Proof.
   - rewrite !and_elim_r wand_elim_r. done.
 Qed.
 
+Lemma wandM_sound (mP : option PROP) Q :
+  (mP -∗? Q) ⊣⊢ (default emp mP -∗ Q).
+Proof. destruct mP; simpl; first done. rewrite emp_wand //. Qed.
+
 (* Pure stuff *)
 Lemma pure_elim φ Q R : (Q ⊢ ⌜φ⌝) → (φ → Q ⊢ R) → Q ⊢ R.
 Proof.
diff --git a/theories/bi/derived_laws_sbi.v b/theories/bi/derived_laws_sbi.v
index 842fcdaa12403c51136789be2435a69e23b7fffd..e1e93317e3141335110f5f980bfefd8ee4254eb2 100644
--- a/theories/bi/derived_laws_sbi.v
+++ b/theories/bi/derived_laws_sbi.v
@@ -247,6 +247,9 @@ Proof. induction n1; f_equiv/=; auto. Qed.
 Lemma laterN_le n1 n2 P : n1 ≤ n2 → ▷^n1 P ⊢ ▷^n2 P.
 Proof. induction 1; simpl; by rewrite -?later_intro. Qed.
 
+Lemma laterN_iter n P : (â–·^n P)%I = Nat.iter n sbi_later P.
+Proof. induction n; f_equal/=; auto. Qed.
+
 Lemma laterN_mono n P Q : (P ⊢ Q) → ▷^n P ⊢ ▷^n Q.
 Proof. induction n; simpl; auto. Qed.
 Global Instance laterN_mono' n : Proper ((⊢) ==> (⊢)) (@sbi_laterN PROP n).
diff --git a/theories/bi/lib/atomic.v b/theories/bi/lib/atomic.v
index 04ce30fa91f670e28ad18573bc53cadb27962f17..09b9ec49ce2c4b107f3732810cc774f7843df175 100644
--- a/theories/bi/lib/atomic.v
+++ b/theories/bi/lib/atomic.v
@@ -160,8 +160,8 @@ Section lemmas.
   Global Instance elim_acc_aacc {X} E1 E2 Ei (α' β' : X → PROP) γ' α β Pas Φ :
     ElimAcc (X:=X) (fupd E1 E2) (fupd E2 E1) α' β' γ'
             (atomic_acc E1 Ei α Pas β Φ)
-            (λ x', atomic_acc E2 Ei α (β' x' ∗ pm_maybe_wand (γ' x') Pas)%I β
-                (λ x y, β' x' ∗ pm_maybe_wand (γ' x') (Φ x y)))%I.
+            (λ x', atomic_acc E2 Ei α (β' x' ∗ (γ' x' -∗? Pas))%I β
+                (λ x y, β' x' ∗ (γ' x' -∗? Φ x y)))%I.
   Proof.
     rewrite /ElimAcc.
     (* FIXME: Is there any way to prevent maybe_wand from unfolding?
diff --git a/theories/bi/telescopes.v b/theories/bi/telescopes.v
new file mode 100644
index 0000000000000000000000000000000000000000..d54533929a945c82d8872083527dacbaaff6251c
--- /dev/null
+++ b/theories/bi/telescopes.v
@@ -0,0 +1,82 @@
+From stdpp Require Export telescopes.
+From iris.bi Require Export bi.
+Set Default Proof Using "Type*".
+Import bi.
+
+(* This cannot import the proofmode because it is imported by the proofmode! *)
+
+(** Telescopic quantifiers *)
+Definition bi_texist {PROP : bi} {TT : tele} (Ψ : TT → PROP) : PROP :=
+  tele_fold (@bi_exist PROP) (λ x, x) (tele_bind Ψ).
+Arguments bi_texist {_ !_} _ /.
+Definition bi_tforall {PROP : bi} {TT : tele} (Ψ : TT → PROP) : PROP :=
+  tele_fold (@bi_forall PROP) (λ x, x) (tele_bind Ψ).
+Arguments bi_tforall {_ !_} _ /.
+
+Notation "'∃..' x .. y , P" := (bi_texist (λ x, .. (bi_texist (λ y, P)) .. )%I)
+  (at level 200, x binder, y binder, right associativity,
+  format "∃..  x  ..  y ,  P") : bi_scope.
+Notation "'∀..' x .. y , P" := (bi_tforall (λ x, .. (bi_tforall (λ y, P)) .. )%I)
+  (at level 200, x binder, y binder, right associativity,
+  format "∀..  x  ..  y ,  P") : bi_scope.
+
+Section telescope_quantifiers.
+  Context {PROP : bi} {TT : tele}.
+
+  Lemma bi_tforall_forall (Ψ : TT → PROP) :
+    bi_tforall Ψ ⊣⊢ bi_forall Ψ.
+  Proof.
+    symmetry. unfold bi_tforall. induction TT as [|X ft IH].
+    - simpl. apply (anti_symm _).
+      + by rewrite (forall_elim TargO).
+      + rewrite -forall_intro; first done.
+        intros p. rewrite (tele_arg_O_inv p) /= //.
+    - simpl. apply (anti_symm _); apply forall_intro; intros a.
+      + rewrite /= -IH. apply forall_intro; intros p.
+        by rewrite (forall_elim (TargS a p)).
+      + move/tele_arg_inv : (a) => [x [pf ->]] {a} /=.
+        setoid_rewrite <- IH.
+        rewrite 2!forall_elim. done.
+  Qed.
+
+  Lemma bi_texist_exist (Ψ : TT → PROP) :
+    bi_texist Ψ ⊣⊢ bi_exist Ψ.
+  Proof.
+    symmetry. unfold bi_texist. induction TT as [|X ft IH].
+    - simpl. apply (anti_symm _).
+      + apply exist_elim; intros p.
+        rewrite (tele_arg_O_inv p) //.
+      + by rewrite -(exist_intro TargO).
+    - simpl. apply (anti_symm _); apply exist_elim.
+      + intros p. move/tele_arg_inv: (p) => [x [pf ->]] {p} /=.
+        by rewrite -exist_intro -IH -exist_intro.
+      + intros x.
+        rewrite /= -IH. apply exist_elim; intros p.
+        by rewrite -(exist_intro (TargS x p)).
+  Qed.
+
+  Global Instance bi_tforall_ne n :
+    Proper (pointwise_relation _ (dist n) ==> dist n) (@bi_tforall PROP TT).
+  Proof.
+    intros ?? EQ. rewrite !bi_tforall_forall. rewrite EQ //.
+  Qed.
+
+  Global Instance bi_tforall_proper :
+    Proper (pointwise_relation _ (⊣⊢) ==> (⊣⊢)) (@bi_tforall PROP TT).
+  Proof.
+    intros ?? EQ. rewrite !bi_tforall_forall. rewrite EQ //.
+  Qed.
+
+  Global Instance bi_texist_ne n :
+    Proper (pointwise_relation _ (dist n) ==> dist n) (@bi_texist PROP TT).
+  Proof.
+    intros ?? EQ. rewrite !bi_texist_exist. rewrite EQ //.
+  Qed.
+
+  Global Instance bi_texist_proper :
+    Proper (pointwise_relation _ (⊣⊢) ==> (⊣⊢)) (@bi_texist PROP TT).
+  Proof.
+    intros ?? EQ. rewrite !bi_texist_exist. rewrite EQ //.
+  Qed.
+
+End telescope_quantifiers.
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 58b7feee3a272384df955d67546f7f7ce47e4d16..15c2f92de46d3170ff944e44fbaa2657d52cd008 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -27,8 +27,8 @@ Tactic Notation "wp_expr_eval" tactic(t) :=
   | _ => fail "wp_expr_eval: not a 'wp'"
   end.
 
-Ltac wp_expr_simpl := wp_expr_eval simpl.
-Ltac wp_expr_simpl_subst := wp_expr_eval simpl_subst.
+Ltac wp_expr_simpl := (wp_expr_eval simpl); pm_prettify.
+Ltac wp_expr_simpl_subst := (wp_expr_eval simpl_subst); pm_prettify.
 
 Lemma tac_wp_pure `{heapG Σ} Δ Δ' s E e1 e2 φ Φ :
   PureExec φ e1 e2 →
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 27fe865a6e30374af760222c7ab3dd7948079d4f..023966eb01f2494650a7a9d950d22c994434681b 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -1,7 +1,7 @@
 From iris.base_logic.lib Require Export fancy_updates.
 From iris.program_logic Require Export language.
 From iris.bi Require Export weakestpre.
-From iris.proofmode Require Import tactics classes.
+From iris.proofmode Require Import base tactics classes.
 Set Default Proof Using "Type".
 Import uPred.
 
@@ -270,9 +270,9 @@ Section proofmode_classes.
     Atomic (stuckness_to_atomicity s) e →
     ElimAcc (X:=X) (fupd E1 E2) (fupd E2 E1)
             α β γ (WP e @ s; E1 {{ Φ }})
-            (λ x, WP e @ s; E2 {{ v, |={E2}=> β x ∗ coq_tactics.pm_maybe_wand (γ x) (Φ v) }})%I.
+            (λ x, WP e @ s; E2 {{ v, |={E2}=> β x ∗ (γ x -∗? Φ v) }})%I.
   Proof.
-    intros ?. rewrite /ElimAcc. setoid_rewrite coq_tactics.pm_maybe_wand_sound.
+    intros ?. rewrite /ElimAcc.
     iIntros "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
     iApply (wp_wand with "[Hinner Hα]"); first by iApply "Hinner".
     iIntros (v) ">[Hβ HΦ]". iApply "HΦ". by iApply "Hclose".
@@ -281,9 +281,9 @@ Section proofmode_classes.
   Global Instance elim_acc_wp_nonatomic {X} E α β γ e s Φ :
     ElimAcc (X:=X) (fupd E E) (fupd E E)
             α β γ (WP e @ s; E {{ Φ }})
-            (λ x, WP e @ s; E {{ v, |={E}=> β x ∗ coq_tactics.pm_maybe_wand (γ x) (Φ v) }})%I.
+            (λ x, WP e @ s; E {{ v, |={E}=> β x ∗ (γ x -∗? Φ v) }})%I.
   Proof.
-    rewrite /ElimAcc. setoid_rewrite coq_tactics.pm_maybe_wand_sound.
+    rewrite /ElimAcc.
     iIntros "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
     iApply wp_fupd.
     iApply (wp_wand with "[Hinner Hα]"); first by iApply "Hinner".
diff --git a/theories/proofmode/class_instances_bi.v b/theories/proofmode/class_instances_bi.v
index 47352dc51822bbf728f6f0b5b44c9187dda617bb..2ebd9d88381ea6cc641afbf0599f75fba975848d 100644
--- a/theories/proofmode/class_instances_bi.v
+++ b/theories/proofmode/class_instances_bi.v
@@ -1,5 +1,5 @@
 From stdpp Require Import nat_cancel.
-From iris.bi Require Import bi tactics.
+From iris.bi Require Import bi tactics telescopes.
 From iris.proofmode Require Import base modality_instances classes ltac_tactics.
 Set Default Proof Using "Type".
 Import bi.
@@ -340,6 +340,16 @@ Global Instance from_modal_bupd `{BiBUpd PROP} P :
 Proof. by rewrite /FromModal /= -bupd_intro. Qed.
 
 (** IntoWand *)
+Global Instance into_wand_wand' p q (P Q P' Q' : PROP) :
+  IntoWand' p q (P -∗ Q) P' Q' → IntoWand p q (P -∗ Q) P' Q' | 100.
+Proof. done. Qed.
+Global Instance into_wand_impl' p q (P Q P' Q' : PROP) :
+  IntoWand' p q (P → Q) P' Q' → IntoWand p q (P → Q) P' Q' | 100.
+Proof. done. Qed.
+Global Instance into_wand_wandM' p q mP (Q P' Q' : PROP) :
+  IntoWand' p q (mP -∗? Q) P' Q' → IntoWand p q (mP -∗? Q) P' Q' | 100.
+Proof. done. Qed.
+
 Global Instance into_wand_wand p q P Q P' :
   FromAssumption q P P' → IntoWand p q (P' -∗ Q) P Q.
 Proof.
@@ -374,6 +384,10 @@ Proof.
   rewrite sep_and [(□ (_ → _))%I]intuitionistically_elim impl_elim_r //.
 Qed.
 
+Global Instance into_wand_wandM p q mP' P Q :
+  FromAssumption q P (pm_default emp%I mP') → IntoWand p q (mP' -∗? Q) P Q.
+Proof. rewrite /IntoWand wandM_sound. exact: into_wand_wand. Qed.
+
 Global Instance into_wand_and_l p q R1 R2 P' Q' :
   IntoWand p q R1 P' Q' → IntoWand p q (R1 ∧ R2) P' Q'.
 Proof. rewrite /IntoWand=> ?. by rewrite /bi_wand_iff and_elim_l. Qed.
@@ -399,6 +413,10 @@ Global Instance into_wand_forall {A} p q (Φ : A → PROP) P Q x :
   IntoWand p q (Φ x) P Q → IntoWand p q (∀ x, Φ x) P Q.
 Proof. rewrite /IntoWand=> <-. by rewrite (forall_elim x). Qed.
 
+Global Instance into_wand_tforall {A} p q (Φ : tele_arg A → PROP) P Q x :
+  IntoWand p q (Φ x) P Q → IntoWand p q (∀.. x, Φ x) P Q.
+Proof. rewrite /IntoWand=> <-. by rewrite bi_tforall_forall (forall_elim x). Qed.
+
 Global Instance into_wand_affine p q R P Q :
   IntoWand p q R P Q → IntoWand p q (<affine> R) (<affine> P) (<affine> Q).
 Proof.
@@ -491,6 +509,9 @@ Qed.
 (** FromWand *)
 Global Instance from_wand_wand P1 P2 : FromWand (P1 -∗ P2) P1 P2.
 Proof. by rewrite /FromWand. Qed.
+Global Instance from_wand_wandM mP1 P2 :
+  FromWand (mP1 -∗? P2) (pm_default emp mP1)%I P2.
+Proof. by rewrite /FromWand wandM_sound. Qed.
 Global Instance from_wand_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
   FromWand P Q1 Q2 → FromWand ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
 Proof. by rewrite /FromWand -embed_wand => <-. Qed.
@@ -824,8 +845,11 @@ Global Instance into_or_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
 Proof. by rewrite /IntoOr -embed_or => <-. Qed.
 
 (** FromExist *)
-Global Instance from_exist_exist {A} (Φ : A → PROP): FromExist (∃ a, Φ a) Φ.
+Global Instance from_exist_exist {A} (Φ : A → PROP) : FromExist (∃ a, Φ a) Φ.
 Proof. by rewrite /FromExist. Qed.
+Global Instance from_exist_texist {A} (Φ : tele_arg A → PROP) :
+  FromExist (∃.. a, Φ a) Φ.
+Proof. by rewrite /FromExist bi_texist_exist. Qed.
 Global Instance from_exist_pure {A} (φ : A → Prop) :
   @FromExist PROP A ⌜∃ x, φ x⌝ (λ a, ⌜φ a⌝)%I.
 Proof. by rewrite /FromExist pure_exist. Qed.
@@ -854,6 +878,9 @@ Qed.
 (** IntoExist *)
 Global Instance into_exist_exist {A} (Φ : A → PROP) : IntoExist (∃ a, Φ a) Φ.
 Proof. by rewrite /IntoExist. Qed.
+Global Instance into_exist_texist {A} (Φ : tele_arg A → PROP) :
+  IntoExist (∃.. a, Φ a) Φ | 10.
+Proof. by rewrite /IntoExist bi_texist_exist. Qed.
 Global Instance into_exist_pure {A} (φ : A → Prop) :
   @IntoExist PROP A ⌜∃ x, φ x⌝ (λ a, ⌜φ a⌝)%I.
 Proof. by rewrite /IntoExist pure_exist. Qed.
@@ -889,6 +916,9 @@ Proof. by rewrite /IntoExist -embed_exist => <-. Qed.
 (** IntoForall *)
 Global Instance into_forall_forall {A} (Φ : A → PROP) : IntoForall (∀ a, Φ a) Φ.
 Proof. by rewrite /IntoForall. Qed.
+Global Instance into_forall_tforall {A} (Φ : tele_arg A → PROP) :
+  IntoForall (∀.. a, Φ a) Φ | 10.
+Proof. by rewrite /IntoForall bi_tforall_forall. Qed.
 Global Instance into_forall_affinely {A} P (Φ : A → PROP) :
   IntoForall P Φ → IntoForall (<affine> P) (λ a, <affine> (Φ a))%I.
 Proof. rewrite /IntoForall=> HP. by rewrite HP affinely_forall. Qed.
@@ -929,6 +959,9 @@ Proof. rewrite /IntoForall. apply forall_intro=><-. rewrite -True_emp True_impl
 Global Instance from_forall_forall {A} (Φ : A → PROP) :
   FromForall (∀ x, Φ x)%I Φ.
 Proof. by rewrite /FromForall. Qed.
+Global Instance from_forall_tforall {A} (Φ : tele_arg A → PROP) :
+  FromForall (∀.. x, Φ x)%I Φ.
+Proof. by rewrite /FromForall bi_tforall_forall. Qed.
 Global Instance from_forall_pure {A} (φ : A → Prop) :
   @FromForall PROP A (⌜∀ a : A, φ a⌝)%I (λ a, ⌜ φ a ⌝)%I.
 Proof. by rewrite /FromForall pure_forall. Qed.
@@ -974,6 +1007,10 @@ Proof.
   rewrite /ElimModal=> H Hφ. apply wand_intro_r.
   rewrite wand_curry -assoc (comm _ (â–¡?p' _)%I) -wand_curry wand_elim_l; auto.
 Qed.
+Global Instance elim_modal_wandM φ p p' P P' Q Q' mR :
+  ElimModal φ p p' P P' Q Q' →
+  ElimModal φ p p' P P' (mR -∗? Q) (mR -∗? Q').
+Proof. rewrite /ElimModal !wandM_sound. exact: elim_modal_wand. Qed.
 Global Instance elim_modal_forall {A} φ p p' P P' (Φ Ψ : A → PROP) :
   (∀ x, ElimModal φ p p' P P' (Φ x) (Ψ x)) → ElimModal φ p p' P P' (∀ x, Φ x) (∀ x, Ψ x).
 Proof.
@@ -1011,6 +1048,9 @@ Proof.
   rewrite /AddModal=> H. apply wand_intro_r.
   by rewrite wand_curry -assoc (comm _ P') -wand_curry wand_elim_l.
 Qed.
+Global Instance add_modal_wandM P P' Q mR :
+  AddModal P P' Q → AddModal P P' (mR -∗? Q).
+Proof. rewrite /AddModal wandM_sound. exact: add_modal_wand. Qed.
 Global Instance add_modal_forall {A} P P' (Φ : A → PROP) :
   (∀ x, AddModal P P' (Φ x)) → AddModal P P' (∀ x, Φ x).
 Proof.
diff --git a/theories/proofmode/class_instances_sbi.v b/theories/proofmode/class_instances_sbi.v
index a502d691ea7813ab16209d19084d0672a819bc6c..e622f11a80b6d540e27d28f83849600e2e755400 100644
--- a/theories/proofmode/class_instances_sbi.v
+++ b/theories/proofmode/class_instances_sbi.v
@@ -1,6 +1,6 @@
 From stdpp Require Import nat_cancel.
 From iris.bi Require Import bi tactics.
-From iris.proofmode Require Import modality_instances classes class_instances_bi coq_tactics ltac_tactics.
+From iris.proofmode Require Import base modality_instances classes class_instances_bi ltac_tactics.
 Set Default Proof Using "Type".
 Import bi.
 
@@ -499,9 +499,9 @@ Global Instance elim_acc_fupd `{BiFUpd PROP} {X} E1 E2 E α β mγ Q :
   (* FIXME: Why %I? ElimAcc sets the right scopes! *)
   ElimAcc (X:=X) (fupd E1 E2) (fupd E2 E1) α β mγ
           (|={E1,E}=> Q)
-          (λ x, |={E2}=> β x ∗ (pm_maybe_wand (mγ x) (|={E1,E}=> Q)))%I.
+          (λ x, |={E2}=> β x ∗ (mγ x -∗? |={E1,E}=> Q))%I.
 Proof.
-  rewrite /ElimAcc. setoid_rewrite pm_maybe_wand_sound.
+  rewrite /ElimAcc.
   iIntros "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
   iMod ("Hinner" with "Hα") as "[Hβ Hfin]".
   iMod ("Hclose" with "Hβ") as "Hγ". by iApply "Hfin".
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 9d75dee407573398f22f574c239309abe858812a..43b2697330831d60eca6e7e3960bc316eb9d9e00 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -161,13 +161,6 @@ Arguments IntoWand' {_} _ _ _%I _%I _%I : simpl never.
 Hint Mode IntoWand' + + + ! ! - : typeclass_instances.
 Hint Mode IntoWand' + + + ! - ! : typeclass_instances.
 
-Instance into_wand_wand' {PROP : bi} p q (P Q P' Q' : PROP) :
-  IntoWand' p q (P -∗ Q) P' Q' → IntoWand p q (P -∗ Q) P' Q' | 100.
-Proof. done. Qed.
-Instance into_wand_impl' {PROP : bi} p q (P Q P' Q' : PROP) :
-  IntoWand' p q (P → Q) P' Q' → IntoWand p q (P → Q) P' Q' | 100.
-Proof. done. Qed.
-
 Class FromWand {PROP : bi} (P Q1 Q2 : PROP) := from_wand : (Q1 -∗ Q2) ⊢ P.
 Arguments FromWand {_} _%I _%I _%I : simpl never.
 Arguments from_wand {_} _%I _%I _%I {_}.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 2ccfba251032b1299db668b16ec3bcbbefce27d9..b85e0a90fa5c5f6ab63d7d57d23029ed3bb17cae 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -7,8 +7,6 @@ Import env_notations.
 
 Local Notation "b1 && b2" := (if b1 then b2 else false) : bool_scope.
 
-Notation pm_maybe_wand mP Q := (pm_from_option (λ P, P -∗ Q)%I Q%I mP).
-
 (* Coq versions of the tactics *)
 Section bi_tactics.
 Context {PROP : bi}.
@@ -336,10 +334,6 @@ Proof.
   - rewrite /= IH (comm _ Q _) assoc. done.
 Qed.
 
-Lemma pm_maybe_wand_sound mP Q :
-  pm_maybe_wand mP Q ⊣⊢ (default emp mP -∗ Q).
-Proof. destruct mP; simpl; first done. rewrite emp_wand //. Qed.
-
 Global Instance envs_Forall2_refl (R : relation PROP) :
   Reflexive R → Reflexive (envs_Forall2 R).
 Proof. by constructor. Qed.
@@ -996,7 +990,7 @@ Lemma tac_inv_elim {X : Type} Δ Δ' i j φ p Pinv Pin Pout (Pclose : option (X
   (∀ R, ∃ Δ'',
     envs_app false (Esnoc Enil j
       (Pin -∗
-       (∀ x, Pout x -∗ pm_maybe_wand (pm_option_fun Pclose x) (Q' x)) -∗
+       (∀ x, Pout x -∗ pm_option_fun Pclose x -∗? Q' x) -∗
        R
       )%I) Δ'
       = Some Δ'' ∧
diff --git a/theories/proofmode/frame_instances.v b/theories/proofmode/frame_instances.v
index 9dc54746dc9037248587ebc6ef333c3ab5feac07..3dee777bfa9cbfb8c15a6ac6587e29da4bd42b1e 100644
--- a/theories/proofmode/frame_instances.v
+++ b/theories/proofmode/frame_instances.v
@@ -287,10 +287,6 @@ Proof. by rewrite /KnownMakeLaterN /MakeLaterN laterN_True. Qed.
 Global Instance make_laterN_emp `{!BiAffine PROP} n :
   @KnownMakeLaterN PROP n emp emp | 0.
 Proof. by rewrite /KnownMakeLaterN /MakeLaterN laterN_emp. Qed.
-Global Instance make_laterN_0 P : MakeLaterN 0 P P | 0.
-Proof. by rewrite /MakeLaterN. Qed.
-Global Instance make_laterN_1 P : MakeLaterN 1 P (â–· P) | 2.
-Proof. by rewrite /MakeLaterN. Qed.
 Global Instance make_laterN_default P : MakeLaterN n P (â–·^n P) | 100.
 Proof. by rewrite /MakeLaterN. Qed.
 
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 81d0a3e5e93100d0ae0e22484b64a4f2f151e401..724c9dcf4e048cc26e9cdf34b5e694476448472e 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -1,6 +1,6 @@
 From iris.proofmode Require Import coq_tactics reduction.
 From iris.proofmode Require Import base intro_patterns spec_patterns sel_patterns.
-From iris.bi Require Export bi.
+From iris.bi Require Export bi telescopes.
 From stdpp Require Import namespaces.
 From iris.proofmode Require Export classes notation.
 From stdpp Require Import hlist pretty.
@@ -293,7 +293,7 @@ Tactic Notation "iPureIntro" :=
 
 (** Framing *)
 Local Ltac iFrameFinish :=
-  lazy iota beta;
+  pm_prettify;
   try match goal with
   | |- envs_entails _ True => by iPureIntro
   | |- envs_entails _ emp => iEmpIntro
@@ -408,7 +408,7 @@ Local Tactic Notation "iIntro" "(" simple_intropattern(x) ")" :=
        [iSolveTC ||
               let P := match goal with |- FromForall ?P _ => P end in
               fail "iIntro: cannot turn" P "into a universal quantifier"
-       |lazy beta; intros x]
+       |pm_prettify; intros x]
      end).
 
 Local Tactic Notation "iIntro" constr(H) :=
@@ -811,7 +811,8 @@ Tactic Notation "iApplyHyp" constr(H) :=
     [eapply tac_apply with _ H _ _ _;
       [pm_reflexivity
       |iSolveTC
-      |pm_reduce (* reduce redexes created by instantiation *)]
+      |pm_prettify (* reduce redexes created by instantiation *)
+      ]
     |iSpecializePat H "[]"; last go H] in
   iExact H ||
   go H ||
@@ -999,7 +1000,7 @@ Tactic Notation "iExists" uconstr(x1) :=
     [iSolveTC ||
      let P := match goal with |- FromExist ?P _ => P end in
      fail "iExists:" P "not an existential"
-    |cbv beta; eexists x1].
+    |pm_prettify; eexists x1].
 
 Tactic Notation "iExists" uconstr(x1) "," uconstr(x2) :=
   iExists x1; iExists x2.
@@ -1058,7 +1059,8 @@ Tactic Notation "iModIntro" uconstr(sel) :=
      end
     |pm_reduce; iSolveTC ||
      fail "iModIntro: cannot filter spatial context when goal is not absorbing"
-    |].
+    |pm_prettify (* reduce redexes created by instantiation *)
+    ].
 Tactic Notation "iModIntro" := iModIntro _.
 Tactic Notation "iAlways" := iModIntro.
 
@@ -1880,7 +1882,7 @@ Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) :=
        let P := match goal with |- IntoInternalEq ?P _ _ ⊢ _ => P end in
        fail "iRewrite:" P "not an equality"
       |iRewriteFindPred
-      |intros ??? ->; reflexivity|lazy beta; iClearHyp Heq]).
+      |intros ??? ->; reflexivity|pm_prettify; iClearHyp Heq]).
 
 Tactic Notation "iRewrite" open_constr(lem) := iRewriteCore Right lem.
 Tactic Notation "iRewrite" "-" open_constr(lem) := iRewriteCore Left lem.
@@ -1899,7 +1901,7 @@ Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) "in" constr(H)
        fail "iRewrite:" P "not an equality"
       |iRewriteFindPred
       |intros ??? ->; reflexivity
-      |pm_reflexivity|lazy beta; iClearHyp Heq]).
+      |pm_reflexivity|pm_prettify; iClearHyp Heq]).
 
 Tactic Notation "iRewrite" open_constr(lem) "in" constr(H) :=
   iRewriteCore Right lem in H.
@@ -2007,7 +2009,7 @@ Tactic Notation "iInvCore" constr(select) "with" constr(pats) "as" open_constr(H
      iSpecializePat H pats; last (
        iApplyHyp H; clear R; pm_reduce;
        (* Now the goal is
-          [∀ x, Pout x -∗ pm_maybe_wand (pm_option_fun Pclose x) (Q' x)],
+          [∀ x, Pout x -∗ pm_option_fun Pclose x -∗? Q' x],
           reduced because we can rely on Pclose being a constructor. *)
        let x := fresh in
        iIntros (x);
@@ -2193,6 +2195,8 @@ Hint Extern 0 (envs_entails _ (big_opMS _ _ _)) =>
 Hint Extern 0 (envs_entails _ (∀ _, _)) => iIntros.
 Hint Extern 0 (envs_entails _ (_ → _)) => iIntros.
 Hint Extern 0 (envs_entails _ (_ -∗ _)) => iIntros.
+(* Multi-intro doesn't work for custom binders. *)
+Hint Extern 0 (envs_entails _ (∀.. _, _)) => iIntros (?).
 
 Hint Extern 1 (envs_entails _ (_ ∧ _)) => iSplit.
 Hint Extern 1 (envs_entails _ (_ ∗ _)) => iSplit.
@@ -2202,6 +2206,7 @@ Hint Extern 1 (envs_entails _ (<pers> _)) => iAlways.
 Hint Extern 1 (envs_entails _ (<affine> _)) => iAlways.
 Hint Extern 1 (envs_entails _ (â–¡ _)) => iAlways.
 Hint Extern 1 (envs_entails _ (∃ _, _)) => iExists _.
+Hint Extern 1 (envs_entails _ (∃.. _, _)) => iExists _.
 Hint Extern 1 (envs_entails _ (â—‡ _)) => iModIntro.
 Hint Extern 1 (envs_entails _ (_ ∨ _)) => iLeft.
 Hint Extern 1 (envs_entails _ (_ ∨ _)) => iRight.
diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index 3dcd333e73d5aee1d08fe0151f4556d6fe0321ba..5d85ca71d0636797ebe12c4bcadf9a83204b5938 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -1,6 +1,6 @@
 From iris.bi Require Export monpred.
 From iris.bi Require Import plainly.
-From iris.proofmode Require Import tactics modality_instances coq_tactics.
+From iris.proofmode Require Import tactics modality_instances.
 
 Class MakeMonPredAt {I : biIndex} {PROP : bi} (i : I)
       (P : monPred I PROP) (𝓟 : PROP) :=
@@ -557,12 +557,11 @@ Proof. by rewrite /MakeMonPredAt /ElimModal monPred_at_fupd=><-. Qed.
 Global Instance elim_acc_at_fupd `{BiFUpd PROP} {X : Type} E1 E2 E
        M1 M2 α β (mγ : X → option PROP) Q (Q' : X → monPred) i :
   ElimAcc (X:=X) M1 M2 α β mγ (|={E1,E}=> Q i)
-          (λ x, |={E2}=> β x ∗ (pm_maybe_wand (mγ x) (|={E1,E}=> Q' x i)))%I →
+          (λ x, |={E2}=> β x ∗ (mγ x -∗? |={E1,E}=> Q' x i))%I →
   ElimAcc (X:=X) M1 M2 α β mγ ((|={E1,E}=> Q) i)
           (λ x, (|={E2}=> ⎡β x⎤ ∗
-                         (pm_maybe_wand
-                            (match mγ x with Some 𝓟 => Some ⎡𝓟⎤ | None => None end)
-                            (|={E1,E}=> Q' x))) i)%I
+                         (match mγ x with Some 𝓟 => Some ⎡𝓟⎤ | None => None end -∗?
+                            |={E1,E}=> Q' x)) i)%I
   | 1.
 Proof.
   rewrite /ElimAcc monPred_at_fupd=><-. apply bi.forall_mono=>x.
@@ -575,12 +574,11 @@ fails. *)
 Global Instance elim_acc_at_fupd_unit `{BiFUpd PROP} E1 E2 E
        M1 M2 α β mγ Q Q' i :
   ElimAcc (X:=unit) M1 M2 α β mγ (|={E1,E}=> Q i)
-          (λ x, |={E2}=> β x ∗ (pm_maybe_wand (mγ x) (|={E1,E}=> Q' i)))%I →
+          (λ x, |={E2}=> β x ∗ (mγ x -∗? |={E1,E}=> Q' i))%I →
   ElimAcc (X:=unit) M1 M2 α β mγ ((|={E1,E}=> Q) i)
           (λ x, (|={E2}=> ⎡β x⎤ ∗
-                         (pm_maybe_wand
-                            (match mγ x with Some 𝓟 => Some ⎡𝓟⎤ | None => None end)
-                            (|={E1,E}=> Q'))) i)%I
+                         (match mγ x with Some 𝓟 => Some ⎡𝓟⎤ | None => None end -∗?
+                            |={E1,E}=> Q')) i)%I
   | 0.
 Proof. exact: elim_acc_at_fupd. Qed.
 
diff --git a/theories/proofmode/reduction.v b/theories/proofmode/reduction.v
index 79046c3d08d7d9445c3b35d8f24b7e7c26f7a5fd..79dde2343a149d9280045ad2d44df568d441fc6c 100644
--- a/theories/proofmode/reduction.v
+++ b/theories/proofmode/reduction.v
@@ -1,9 +1,8 @@
-From iris.bi Require Import bi.
+From iris.bi Require Import bi telescopes.
 From iris.proofmode Require Import base environments.
 
 Declare Reduction pm_cbv := cbv [
   (* base *)
-  pm_option_bind pm_from_option pm_option_fun
   base.beq base.Pos_succ base.ascii_beq base.string_beq base.positive_beq base.ident_beq
   (* environments *)
   env_lookup env_lookup_delete env_delete env_app env_replace
@@ -13,9 +12,28 @@ Declare Reduction pm_cbv := cbv [
   envs_clear_spatial envs_clear_persistent envs_incr_counter
   envs_split_go envs_split prop_of_env
 ].
+(* Some things should only be unfolded according to cbn rules, when
+   certain arguments are constructors. This is because they can appear in
+   the user side of proofs as well. *)
+Declare Reduction pm_cbn := cbn [
+  (* PM option combinators *)
+  pm_option_bind pm_from_option pm_option_fun
+  (* telescope combinators *)
+  tele_fold tele_bind tele_app
+  (* BI connectives *)
+  bi_persistently_if bi_affinely_if bi_intuitionistically_if
+  bi_wandM sbi_laterN big_opL
+  bi_tforall bi_texist
+].
 Ltac pm_eval t :=
   let u := eval pm_cbv in t in
-  u.
+  let v := eval pm_cbn in u in
+  v.
 Ltac pm_reduce :=
   match goal with |- ?u => let v := pm_eval u in change v end.
 Ltac pm_reflexivity := pm_reduce; exact eq_refl.
+
+(** Called e.g. by iApply for redexes that are created by instantiation.
+    This cannot create any envs redexes so we just to the cbn part. *)
+Ltac pm_prettify :=
+  match goal with |- ?u => let v := eval pm_cbn in u in change v end.