Get rid of `FromLaterN` class.

This class was used to allow iNext (currently iModIntro) to succeed on goals like:

▷ P ∗ ▷ Q

It turns out that this feature is barely used and unnecessary complicates things, especially now that iModIntro can be used to introduce any modality. This complication arises both conceptually and technically:

• For other modalities, e.g. |==>, ◇, □ the tactic would fail if the modality does not appear at the top-level but was distributed among other connectives. It's confusing that the distribution works for ▷ but not for other connectives.
• If we wish to support this kind of distribution of connectives for any modality, the complexity becomes really bad. When running iModIntro it should for each modality traverse the whole goal, giving rise to a complexity of num_modalities * size_of_the_goal when iModIntro is called without the modality being specified.