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