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