Sequent

[iehality]

Add framework for sequent calculi.

class SequentCalc₁ {F : outParam Type*}
    (R : outParam Type*) [Precollection F R] (S : Type*) where
  Sqt : S → R → Type*

notation:45 "⊢[" 𝓢 "] " Γ:46 => SequentCalc₁.Sqt 𝓢 Γ

class SequentCalc₂ {F : outParam Type*}
    (L R : outParam Type*) [Collection F L] [Precollection F R] (S : Type*) where
  Sqt : S → L → R → Type*

notation:45 Δ:45 " ⟹[" 𝓢 "] " Γ:46 => SequentCalc₂.Sqt 𝓢 Δ Γ