intro b hi a
case hs

⊢ ∀ (n : ↑N0), (∀ (a : ↑N0), plus (S a, n) = S (plus (a, n))) → ∀ (a : ↑N0), plus (S a, S n) = S (plus (a, S n))
case hs
b : ↑N0
hi : ∀ (a : ↑N0), plus (S a, b) = S (plus (a, b))
a : ↑N0
⊢ plus (S a, S b) = S (plus (a, S b))