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