intros n hi y
case hs

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