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