diff --git a/ProofMode.md b/ProofMode.md
index 8583f742e2cf6b95ca15d4d1c3c4cd727a042de7..a97d988d072bf7fdb32430341adff7d5ecbea06e 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -16,6 +16,12 @@ Applying hypotheses and lemmas
 - `iApply pm_trm` : match the conclusion of the current goal against the
   conclusion of `pm_trm` and generates goals for the premises of `pm_trm`. See
   proof mode terms below.
+  If the applied term has more premises than the number of given specialization
+  patterns, all remaining spatial hypotheses go to the first premise that does
+  not have corresponding specialization pattern. Subsequent premises without
+  specialization pattern do not get any spatial hypotheses. In other words, the
+  specialization pattern is extended with `[-] [] ... []` to account for
+  hypotheses without specialization pattern.
 
 Context management
 ------------------