Been feeling increasingly sick today since about noonish. Finding it kind of hard to sustain much of an attention span through stabby stomach pain, but I read enough of [Miller Nadathur Pfenning Scedrov '89] to kind of grasp that the point of hereditary Harrop formulae is that they are the sublanguage of sequents where it's safe to always focus on the right if at all possible. (i.e. if you don't have an atomic proposition there) At least I hope that's right, because that's the conclusion I came to.