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