Coherent sequent ($\varphi {⊢}_{\vec{x}}\psi$)

A coherent sequent is an implication $\varphi {⊢}_{\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.