intros n
case a
a b : String
n : ℕ
ab : a = b
⊢ ∀ (n : ℕ), Ø ⋁ fromNat n +ₛ fromNat n =ₛ fromNat n +ₛ fromNat n
case a
a b : String
n✝ : ℕ
ab : a = b
n : ℕ
⊢ Ø ⋁ fromNat n +ₛ fromNat n =ₛ fromNat n +ₛ fromNat n