DEFINITION r_arith0()
TYPE =
       ∀k:K.∀i:nat.(eq nat (minus (r k (S i)) (S O)) (r k i))
BODY =
        assume k: K
        assume i: nat
          (h1) 
             (h1) 
                by (refl_equal . .)
eq nat (r k i) (r k i)
             end of h1
             (h2) 
                by (minus_Sx_SO .)
eq nat (minus (S (r k i)) (S O)) (r k i)
             end of h2
             by (eq_ind_r . . . h1 . h2)
eq nat (minus (S (r k i)) (S O)) (r k i)
          end of h1
          (h2) 
             by (r_S . .)
eq nat (r k (S i)) (S (r k i))
          end of h2
          by (eq_ind_r . . . h1 . h2)
          we proved eq nat (minus (r k (S i)) (S O)) (r k i)
       we proved ∀k:K.∀i:nat.(eq nat (minus (r k (S i)) (S O)) (r k i))