G1 |- D1 | G2 |- D2 | ... Gn |- Dn
and just a plain old sequent in a standard hybrid system with a distinct label for each sequent, like
G1[a1], G2[a2] ... Gn[an] |- D1[a1], D2[a2], ... Dn[an]
In which case the sequent rules Restall gave for S5 box seem to be exactly those that I'd expect for ∀a.A @ a, as it shows up in tom7's thesis for example. On the left, you get to pick a label, or equivalently the sequent within the hypersequent that you travel to, and on the right you create a fresh label, which is equivalent to creating a fresh sequent disjunctively adjoined to all the rest.
