diff --git a/ProofMode.md b/ProofMode.md
index 17ccf47b877484647d486caa271fbe354b6d6069..3bb6cc0447c1590d511f76b918f2f5054a7c0c9c 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -124,8 +124,8 @@ The later modality
 
 - `iNext n` : introduce `n` laters by stripping that number of laters from all
   hypotheses. If the argument `n` is not given, it strips one later if the
-  leftmost conjuct is of the shape `â–· P`, or `n` laters if the leftmost conjuct
-  is of the shape `â–·^n P`.
+  leftmost conjunct is of the shape `â–· P`, or `n` laters if the leftmost
+  conjunct is of the shape `â–·^n P`.
 - `iLöb as "IH" forall (x1 ... xn) "selpat"` : perform Löb induction by
   generating a hypothesis `IH : â–· goal`. The tactic generalizes over the Coq
   level variables `x1 ... xn`, the hypotheses given by the selection pattern