intros m
case a
a b : String
n : ℕ
nab : ¬a = b
⊢ ∀ (n_1 : ℕ), Ø ⋁ fromNat n +ₛ _ b =ₛ _ b +ₛ fromNat n [b ≔ fromNat n_1]
case a
a b : String
n : ℕ
nab : ¬a = b
m : ℕ
⊢ Ø ⋁ fromNat n +ₛ _ b =ₛ _ b +ₛ fromNat n [b ≔ fromNat m]