diff --git a/ProofMode.md b/ProofMode.md
index 9232ac054decdcc3cf03362e79ab1c7b0ffd39f3..4f14da9f32956fbd64c9d3f31e9945cc5ec2b5cf 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -100,6 +100,13 @@ The later modality
 - `iLöb (x1 ... xn) as "IH"` : perform Löb induction by generalizing over the
   Coq level variables `x1 ... xn` and the entire spatial context.
 
+Induction
+---------
+- `iInduction x as cpat "IH"` : perform induction on the Coq term `x`. The Coq
+  introduction pattern is used to name the introduced variables. The induction
+  hypotheses are inserted into the persistent context and given fresh names
+  prefixed `IH`.
+
 Rewriting
 ---------