cases nf
α : Sinf
x : String
Δ : Ctx Sinf
nf : Δ ⋁ ¬ₛ (∀ₛ x ; α)
⊢ ∃ θ, Δ ⋁ ¬ₛ α [x ≔ θ]
case S_weakening
α : Sinf
x : String
δ✝ : Sinf
Δ✝ : Ctx Sinf
a✝ : Δ✝ ⋁ δ✝
⊢ ∃ θ, δ✝ :: Δ✝ ⋁ ¬ₛ α [x ≔ θ]

case S_neg_forall
α : Sinf
x : String
Δ : Ctx Sinf
θ✝ : Sinf_term
a✝ : Δ ⋁ ¬ₛ α [x ≔ θ✝]
⊢ ∃ θ, Δ ⋁ ¬ₛ α [x ≔ θ]