Define persistence otherwise (and get rid of core)
As a preparatory step towards defining the persistence modality inside the logic (if reasonably possible), we could try to change the model of persistence in Iris to no longer use the core (and get rid of the core). As long as persistence is the only connective defined using the core, it is impossible to define an equivalent connective inside the logic, so this is interesting both to simplify the RA axioms (and even more so the axioms for ordered RAs), and to work towards maybe eventually defining persistence inside the logic.