This MR introduces the following primitive soundness statements:
- Soundness of pure propositions
⌜ φ ⌝%I → φ. - Soundness of later
(▷ P)%I → P.
The old soundness statement, (▷^n ⌜ φ ⌝)%I → φ is now a derived form.
I think having (▷ P)%I → P is quite common in modal logic, so it's nice that we it too.