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)