Support clear patterns in more places

Right now, one can write iIntros "{Hfoo} [Hfoo Hbar]", but if I do iMod ... as "{Hshr} [Hshr $]", I get

Tactic failure: invalid intro_pat "{Hshr} [Hshr $]".

(See https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/master/theories/typing/own.v#L134)