cases ih
a : String
n : ℕ
ih : Ø ⋁ ¬ₛ fromNat n↗ =ₛ O
⊢ Ø ⋁ ¬ₛ fromNat n↗↗ =ₛ O
case S_axiom_neg
a : String
n : ℕ
nv₁✝ : NoVars (fromNat n↗)
nv₂✝ : NoVars O
a✝ : Sinf_const.eval (Sinf_const.coerce (fromNat n↗) nv₁✝) ≠ Sinf_const.eval (Sinf_const.coerce O nv₂✝)
⊢ Ø ⋁ ¬ₛ fromNat n↗↗ =ₛ O