This change I'm helping shepherd into Iris-Lean is somehow radicalizing me even more. We're working on changing the algebraic hierarchy to be based on ORA's instead of CMRA's, but because Lean has good typeclasses, we can actually do this swap Indiana Jones style with essentially zero impact on clients who use CMRA. It's kind of like how Iris-Rocq has a MRA construction, but you'll notice.... no MRA canonical structures. I understand that this kind of thing is very hard to do in that system (hard enough to necessitate a fork). Not a problem in Lean.