Syntax `iAssert (Q with spat) as ...`

This is more consistent with the with syntax in iSpecialize, iDestruct, and friends.

As a positive addition, it also makes the code shorter.