apply S_out
case a.a
α β : Sinf
Δ : Ctx Sinf
contr : Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
iβ : Δ ⋁ β ∨ₛ ¬ₛ (α ∨ₛ ¬ₛ α)
s_return : β :: Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
n : β :: Δ ⋁ ¬ₛ α
nn : β :: Δ ⋁ ¬ₛ ¬ₛ α
⊢ Δ ⋁ β ∨ₛ ¬ₛ α
case a.a.a
α β : Sinf
Δ : Ctx Sinf
contr : Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
iβ : Δ ⋁ β ∨ₛ ¬ₛ (α ∨ₛ ¬ₛ α)
s_return : β :: Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
n : β :: Δ ⋁ ¬ₛ α
nn : β :: Δ ⋁ ¬ₛ ¬ₛ α
⊢ β :: Δ ⋁ ¬ₛ α