cases _12
θ₁ θ₂ θ₃ : Sinf_term
Δ : Ctx Sinf
_12 : Δ ⋁ θ₁ =ₛ θ₂
_23 : Δ ⋁ θ₂ =ₛ θ₃
⊢ Δ ⋁ θ₁ =ₛ θ₃
case S_axiom
θ₁ θ₂ θ₃ : Sinf_term
Δ : Ctx Sinf
_23 : Δ ⋁ θ₂ =ₛ θ₃
nv₁✝ : NoVars θ₁
nv₂✝ : NoVars θ₂
a✝ : Sinf_const.eval (Sinf_const.coerce θ₁ nv₁✝) = Sinf_const.eval (Sinf_const.coerce θ₂ nv₂✝)
⊢ Δ ⋁ θ₁ =ₛ θ₃

case S_weakening
θ₁ θ₂ θ₃ : Sinf_term
δ✝ : Sinf
Δ✝ : Ctx Sinf
a✝ : Δ✝ ⋁ δ✝
_23 : δ✝ :: Δ✝ ⋁ θ₂ =ₛ θ₃
⊢ δ✝ :: Δ✝ ⋁ θ₁ =ₛ θ₃