diff --git a/iris_heap_lang/proofmode.v b/iris_heap_lang/proofmode.v
index 031de179b6382fefbcb7a193f5f5c4c13f77a6e9..fa98c676267f0bf48cdfb7da17c8c7e57d67886b 100644
--- a/iris_heap_lang/proofmode.v
+++ b/iris_heap_lang/proofmode.v
@@ -385,7 +385,7 @@ Proof.
   rewrite -wp_bind. eapply wand_apply; first by eapply wp_xchg.
   rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
   rewrite right_id.
-    by apply later_mono, sep_mono_r, wand_mono.
+  by apply later_mono, sep_mono_r, wand_mono.
 Qed.
 Lemma tac_twp_xchg Δ s E i K l v v' Φ :
   envs_lookup i Δ = Some (false, l ↦ v)%I →