The common principle is "unnesting an index borrow". This simplifies
the proofs of reborrowing and unnesting, and, moreover, gives a slightly
stronger unnesting rule (the masks are different).