case a.succ.zero n ih =>
  rcases ih with ⟨⟨⟩, ⟨⟩, e⟩
  constructor <;> try constructor <;> try constructor <;> try assumption
  simp at *
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↗
no goals