Unify `iNext` and `iModIntro` (and more?)
These tactics are very similar. I would be nice to generalize
iModIntro to also strip occurrences of the modality from all of the hypotheses.
Given that we have already generalized
iNext to deal with the iterated later modality, I think this should not be too difficult.
See also the discussion as part of commit 9ae19ed5.