DEFINITION s_plus()
TYPE =
       ∀k:K.∀i:nat.∀j:nat.(eq nat (s k (plus i j)) (plus (s k i) j))
BODY =
Show proof