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