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.