Fix to Fabien Renaud's comment about adequacy: in order for the calculus in Agda to correspond to the one in the paper, it's necessary to add a new condition to ^L that the succedent U is stable. This already was applied to the Twelf development; it's quite straightforward to add here and mostly pops up here and there in unfocused admissibility, which uses shifts extensively.