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.