induction n <;> induction m <;> simp at *
case a
a b : String
n : ℕ
nab : ¬a = b
m : ℕ
⊢ Ø ⋁ Sinf_term.subst (fromNat n) b (fromNat m) +ₛ fromNat m =ₛ fromNat m +ₛ Sinf_term.subst (fromNat n) b (fromNat m)
case a.zero.zero
a b : String
nab : ¬a = b
⊢ Ø ⋁ O +ₛ O =ₛ O +ₛ O

case a.zero.succ
a b : String
nab : ¬a = b
n✝ : ℕ
n_ih✝ : Ø ⋁ O +ₛ fromNat n✝ =ₛ fromNat n✝ +ₛ O
⊢ Ø ⋁ O +ₛ fromNat n✝↗ =ₛ fromNat n✝↗ +ₛ O

case a.succ.zero
a b : String
nab : ¬a = b
n✝ : ℕ
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 a.succ.succ
a b : String
nab : ¬a = b
n✝¹ n✝ : ℕ
n_ih✝¹ :
  Ø ⋁
      Sinf_term.subst (fromNat n✝¹) b (fromNat n✝) +ₛ fromNat n✝ =ₛ
        fromNat n✝ +ₛ Sinf_term.subst (fromNat n✝¹) b (fromNat n✝) →
    Ø ⋁
      Sinf_term.subst (fromNat n✝¹) b (fromNat n✝)↗ +ₛ fromNat n✝ =ₛ
        fromNat n✝ +ₛ Sinf_term.subst (fromNat n✝¹) b (fromNat n✝)↗
n_ih✝ :
  Ø ⋁
    Sinf_term.subst (fromNat n✝¹) b (fromNat n✝↗) +ₛ fromNat n✝↗ =ₛ
      fromNat n✝↗ +ₛ Sinf_term.subst (fromNat n✝¹) b (fromNat n✝↗)
⊢ Ø ⋁
    Sinf_term.subst (fromNat n✝¹) b (fromNat n✝↗)↗ +ₛ fromNat n✝↗ =ₛ
      fromNat n✝↗ +ₛ Sinf_term.subst (fromNat n✝¹) b (fromNat n✝↗)↗