diff --git a/docs/proof_mode.md b/docs/proof_mode.md
index 5aa8b3e84dc4c047aa9dc17da1c6c1b1430f6ab2..dca9f23dfaa650de2f0c191b7929ae0c27bba143 100644
--- a/docs/proof_mode.md
+++ b/docs/proof_mode.md
@@ -134,8 +134,8 @@ Modalities
   and subjectively. The optional argument `mod` can be used to specify what
   modality to introduce in case of ambiguity, e.g. `⎡|==> P⎤`.
 - `iAlways` : a deprecated alias of `iModIntro`.
-- `iNext n` : an alias of `iModIntro (â–·^n P)`.
-- `iNext` : an alias of `iModIntro (â–·^1 P)`.
+- `iNext n` : an alias of `iModIntro (â–·^n _)`.
+- `iNext` : an alias of `iModIntro (â–·^_ _)`.
 - `iMod pm_trm as (x1 ... xn) "ipat"` : eliminate a modality `pm_trm` that is
   an instance of the `ElimModal` type class. Instances include: later, except 0,
   basic update and fancy update.