Persistently: Get rid of mono and idemp in favor of intro
Turns out that
intro is strong enough to derive both
idemp. I think having
elim primitive is neater; this also matches the usual presentation of
! in (intuitionistic) linear logic. If you agree, I can do the same for plainly.
Of course, I find this right after I tagged Iris 3.1.0.