box turns a box modal formula [a]P equivalently into a double negated diamond modal formula ¬⟨a⟩¬P. This is occasionally useful to convert between box and diamond modalities to make use of suitable proof rules that require a particular shape or side of the sequent.