cases d
α β : Sinf
Δ : Ctx Sinf
d : Δ ⋁ ¬ₛ (α ∨ₛ β)
⊢ (Δ ⋁ ¬ₛ α) ∧ (Δ ⋁ ¬ₛ β)
case S_weakening
α β δ✝ : Sinf
Δ✝ : Ctx Sinf
a✝ : Δ✝ ⋁ δ✝
⊢ (δ✝ :: Δ✝ ⋁ ¬ₛ α) ∧ (δ✝ :: Δ✝ ⋁ ¬ₛ β)

case S_de_morgan
α β : Sinf
Δ : Ctx Sinf
a✝¹ : Δ ⋁ ¬ₛ α
a✝ : Δ ⋁ ¬ₛ β
⊢ (Δ ⋁ ¬ₛ α) ∧ (Δ ⋁ ¬ₛ β)