Support destructing exists with intro patterns

This is a version of !483 (closed) (by @tchajed) that uses a different approach for backwards compatibility.

The MR enables [% ...] to be used as a pattern to destruct existentials, and (with the string-ident plugin) [%name ...] to give a name to the witness. To maintain backwards compatibility, the same pattern can also still be used to destruct (separating) conjunctions where the left-hand side is pure. For terms that are syntactically conjunctions, this would not even require further changes (the existing IntoExist instances already support that); but to also support ⌜φ ∧ ψ⌝ we add a new instance for convenience.

Fixes #310 (closed)

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, 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.