rcases ih with ⟨⟨⟩, ⟨⟩, e⟩
a b : String
nab : ¬a = b
n : ℕ
ih : Ø ⋁ Sinf_term.subst (fromNat n) b O +ₛ O =ₛ O +ₛ Sinf_term.subst (fromNat n) b O
⊢ Ø ⋁ Sinf_term.subst (fromNat n) b O↗ +ₛ O =ₛ O +ₛ Sinf_term.subst (fromNat n) b O↗
case S_axiom.plus.plus
a b : String
nab : ¬a = b
n : ℕ
a✝³ : NoVars (Sinf_term.subst (fromNat n) b O)
a✝² a✝¹ : NoVars O
a✝ : NoVars (Sinf_term.subst (fromNat n) b O)
e :
  Sinf_const.eval (Sinf_const.coerce (Sinf_term.subst (fromNat n) b O +ₛ O) (NoVars.plus a✝³ a✝²)) =
    Sinf_const.eval (Sinf_const.coerce (O +ₛ Sinf_term.subst (fromNat n) b O) (NoVars.plus a✝¹ a✝))
⊢ Ø ⋁ Sinf_term.subst (fromNat n) b O↗ +ₛ O =ₛ O +ₛ Sinf_term.subst (fromNat n) b O↗