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

case S_weakening
θ₁ θ₂ θ₃ : Sinf_term
nv₁ : NoVars θ₁
nv₂ : NoVars θ₂
e : Sinf_const.eval (Sinf_const.coerce θ₁ nv₁) = Sinf_const.eval (Sinf_const.coerce θ₂ nv₂)
δ✝ : Sinf
Δ✝ : Ctx Sinf
a✝ : Δ✝ ⋁ δ✝
⊢ δ✝ :: Δ✝ ⋁ θ₁ =ₛ θ₃