apply generic_recursor
⊢ ∀ (b a : ↑N0), plus (S a, b) = S (plus (a, b))
case hz

⊢ ∀ (a : ↑N0), plus (S a, z) = S (plus (a, z))

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))