Add `with M` option to `iModIntro` and use to redefine `iNext` to fix issue #331
This allows us to not just specify a matching subterm for
iModIntro, but also exactly what modality to introduce. This allows us to redefine
iNext so that issue #331 can be closed.
I don't quite like the
with syntax, so suggestions for improvement are welcome.