Persistently: Get rid of mono and idemp in favor of intro
Turns out that intro
is strong enough to derive both mono
and idemp
. I think having intro
and 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.