Support destructing exists with intro patterns
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)