extend proof_mode.md

docs/proof_mode.md

@@ -328,6 +328,9 @@ _introduction patterns_:
   + Either the proposition `P` or `Q` should be persistent.
   + Either `ipat1` or `ipat2` should be `_`, which results in one of the
     conjuncts to be thrown away.
+- `[% ipat]` : existential elimination. Falls back to (separating) conjunction
+  elimination in case the hypothesis is not an existential, so this pattern also
+  works for (separating) conjunctions with a pure left-hand side.
 - `(pat1 & pat2 & ... & patn)` : syntactic sugar for `[pat1 [pat2 .. patn ..]]`
   to destruct nested (separating) conjunctions.
 - `[ipat1|ipat2]` : disjunction elimination.