register make_laterable as modality

Upamanyu (student at MIT) started looking into make_laterable, which made me realize that it might be worth properly registering this as a modality so we can do iModIntro. However, it turns out the old definition of make_laterable is not suited for that: it does not satisfy the lemma

  Lemma make_laterable_intro' Q :
    Laterable Q →
    Q -∗ make_laterable Q.

So, when doing iModIntro on a make_laterable, we couldn't just keep all Laterable things in the context -- we would additionally get an extra ◇ in front of each of them. To fix that I slightly changed the definition of make_laterable; most existing laws still hold (or become stronger), with one exception: there's now a ◇ in

  Lemma make_laterable_elim Q :
    make_laterable Q -∗ ◇ Q.

Still, I think the fact that make_laterable_intro' now holds shows that this is the better definition. Logically atomic triples (the only in-tree user of all this) are unaffected by this change, their API surface remains the same.

I also changed make_laterable_wand to a less surprising statement:

  Lemma make_laterable_wand Q1 Q2 :
    make_laterable (Q1 -∗ Q2) -∗ (make_laterable Q1 -∗ make_laterable Q2).

Sadly, for non-affine BIs, this does not imply the old way of stating that lemma, so that lemma also has to be kept around (under a new name):

  Lemma make_laterable_intuitionistic_wand Q1 Q2 :
    □ (Q1 -∗ Q2) -∗ (make_laterable Q1 -∗ make_laterable Q2).

So, overall I'd say this MR makes make_laterable much more well-behaved and better integrated into the IPM for affine BIs. Figuring out something reasonable for non-affine BIs remains future work.

When there are non-laterable things in the context, iModIntro will add a ▷ in front of them to make them laterable. The same approach is now also used by iAuIntro, though that requires a hack since we cannot actually use idModIntro on make_laterable here.

Future plans: #424