cases f
α : Sinf
x : String
Δ : Ctx Sinf
f : Δ ⋁ ∀ₛ x ; α
⊢ ∀ (n : ℕ), Δ ⋁ α [x ≔ Sinf_term.fromNat n]
case S_weakening
α : Sinf
x : String
δ✝ : Sinf
Δ✝ : Ctx Sinf
a✝ : Δ✝ ⋁ δ✝
⊢ ∀ (n : ℕ), δ✝ :: Δ✝ ⋁ α [x ≔ Sinf_term.fromNat n]

case S_induction
α : Sinf
x : String
Δ : Ctx Sinf
a✝ : ∀ (n : ℕ), Δ ⋁ α [x ≔ Sinf_term.fromNat n]
⊢ ∀ (n : ℕ), Δ ⋁ α [x ≔ Sinf_term.fromNat n]