I've been looking at a modal logic with the axiom
$$ (\Diamond A \land \Diamond B) \to \Diamond((A \land \Diamond B) \vee (A \land B) \vee (A \land \Diamond B)) $$
Roughly, this says that the accessibility relation is linear.
It seems like you can give a proof theory for this language using hypersequents (see Andrzej Indrzejczak's Cut-Free Hypersequent Calculus for S4.3), and I was wondering if anyone has investigated giving proof term assignments to hypersequent calculi.
Alternatively, I'd be just as happy if someone had shown how to translate hypersequent calculi into hybrid logics.