Merged requested to merge robbert/base_logic_soundness into master
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.