Super `iModIntro` tactic that generalizes `iAlways`, `iNext`, `iModIntro`, and more

A new iModIntro tactic that generalizes the former iAlways, iNext and iModIntro. On top of that, it supports introduction of heterogeneous modalities such as bi_embed.

This MR fixes #147 (closed) and #48 (closed).

Todo

• Fix compilation, it needs a newer std++ but the CI is currently broken so no opam packages are published.
• Move the modality stuff from proofmode.classes to its own file?
• Bikeshed about the name.
• What to do with the current iNext? It is currently an alias for iModIntro. We could a.) deprecate it b.) make it a specific version of iModIntro that only works for laters.
• Figure out what introduction pattern to deprecate, !# or !>. (I propose to keep !>).
• The axioms are stronger than what was supported for the old iModIntro, e.g. the current modality needs to satisfy M P ∗ M Q ⊢ M (P ∗ Q). This is not a problem for any of the existing instances, but the relative/subjective modality of monPred does not satisfy this property.
• Fix the instance from_modal_monPred_at : FromModal P Q → MakeMonPredAt i Q 𝓠 → FromModal (P i) 𝓠. I suppose we should give instances for specific modalities. Which? @jjourdan any idea?
• The order in proofmode.classes and proofmode.class_instances is a bit of a mess. I propose to reorder this later to avoid too conflicts with other MRs/master.