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