Coherent sequent
= Coherent sequent
{title2=$\phi\vdash_{\vec x}\psi$}
A coherent sequent is an implication $\phi\vdash_{\vec x}\psi$ between <coherent formulas> in a common context. Its semantics is inclusion of the two interpreted subobjects of that context. The context is universally quantified outside the formulas.