diff --git a/docs/proof_mode.md b/docs/proof_mode.md
index 3071750f5e537a256843e2207dc2c81430276519..296732ee6ad73bb3a4c7cb2a86fb5ea183d0520b 100644
--- a/docs/proof_mode.md
+++ b/docs/proof_mode.md
@@ -248,8 +248,8 @@ Iris
 ----
 
 - `iInv H as (x1 ... xn) "ipat"` : open an invariant in hypothesis H. The result
-   is destructed using the Coq intro patterns `x1 ... xn` (for existential
-   quantifiers) and then the proof mode [introduction pattern][ipat] `ipat`.
+  is destructed using the Coq intro patterns `x1 ... xn` (for existential
+  quantifiers) and then the proof mode [introduction pattern][ipat] `ipat`.
   + `iInv H with "selpat" as (x1 ... xn) "ipat" "Hclose"` : generate an update
   for closing the invariant and put it in a hypothesis named `Hclose`.
   + `iInv H with "selpat" as (x1 ... xn) "ipat"` : supply a selection pattern