<div>
  <p>
  <kbd>boxAnd</kbd> splits a conjunctive postcondition <code>[a](P∧Q)</code> into two separate postconditions that can be proved on separate branches <code>[a]P ∧ [a]Q</code> by using <kbd>andR</kbd>.
  This is an especially clever idea when <code>P</code> and <code>Q</code> hold for very different reasons after <code>a</code>.
</p>
</div>