Put the shift_loc notation in the right scope so that it is parsed/printed properly even when appearing in expressions.

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).

The hypothesis was introduced into the pure context, because it is
convertible to True. IMHO, the ** introduction pattern is not something
that should be used often, so, I replace it.