Simplify under modality

[hferee]

□φ should be simplified to □ψ if φ simplifies to ψ.