Naming bikeshed: Persistently and affinely-persistently

Currently, in gen_proofmode, the name "persistently" and the typeclass "Persistent" do not match the notation □.

I think this is a great name for "the context that behaves like normal intuitionistic logic", so I think ideally we should call □ "persistently" here as well, and define Persistent P := P |- □ P. This requires finding a new name for the modality that is in the BI interface -- the modality that allows duplication, but does not allow throwing things away. IIRC @jtassaro called this modality "relevant". That doesn't seem like the worst possible name, though "relevantly" sounds a little funny?

To be clear, I suggest keeping the name "persistent" for the □ and the "persistent context". If we change that name, it would affect affine Iris, and I don't think we want to rename this symbol there again.