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 0cdf4724164604977f4d0bb2dd7e9c5d0d57f4b7..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
diff --git a/tests/proofmode.v b/tests/proofmode.v
index f558964abcad9ac27c4594941a9caadef7f1b67d..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.
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..004892b1c9d31de207170247cfdc02853f3677c0 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -91,8 +91,14 @@ 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.
 
+(** Iterated later *)
+Lemma laterN_iter n P : (â–·^n P)%I = Nat.iter n sbi_later P.
+Proof. induction n; f_equal/=; auto. 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 024ad12911254e344de4e9d4a3047a5cb22953de..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.
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/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/reduction.v b/theories/proofmode/reduction.v
index 3dd260e5ad55ef731276d936978cb288c7469924..79dde2343a149d9280045ad2d44df568d441fc6c 100644
--- a/theories/proofmode/reduction.v
+++ b/theories/proofmode/reduction.v
@@ -22,7 +22,7 @@ Declare Reduction pm_cbn := cbn [
   tele_fold tele_bind tele_app
   (* BI connectives *)
   bi_persistently_if bi_affinely_if bi_intuitionistically_if
-  bi_wandM big_opL
+  bi_wandM sbi_laterN big_opL
   bi_tforall bi_texist
 ].
 Ltac pm_eval t :=