DEFINITION s_S()
TYPE =
       ∀k:K.∀i:nat.(eq nat (s k (S i)) (S (s k i)))
BODY =
Show proof