A failing iIntros for implications should prettify the identifier before
printing, and iIntros on something that isn't a wand or implication
should say what couldn't be introduced (to clarify that `iIntros "HP
HQ"` failed because of the HQ in particular, for example).

For example, `auth_auth_valid`.

`iDestruct H as "H1 H2"` produces an error that says the pattern should
contain exactly one proper introduction pattern. When multiple patterns
are provided, due to Ltac variable shadowing iDestructHypFindPat was
instead reporting only the first pattern in the error message (and even
that was printed as the parsed AST rather than the original string).

The error handling for `iIntro (?)` and similar tactics didn't correctly
report failures when the goal couldn't be turned into a universal
quantifier. This is something missing from !482 due to no test
triggering the error.

Fixes a bug from iris/iris!488

The old code contained a bunch of unused spaghetti that was not cleaned up
after a refactoring.

@jihgfee menaged to trigger a wrong code path in the old code, but I failed
to turn his test case into a self-contained one.