DEFINITION s_arith0()
TYPE =
       ∀k:K.∀i:nat.(eq nat (minus (s k i) (s k O)) i)
BODY =
        assume k: K
        assume i: nat
          (h1) 
             by (minus_n_O .)
             we proved eq nat i (minus i O)
             we proceed by induction on the previous result to prove eq nat (minus i O) i
                case refl_equal : ⇒
                   the thesis becomes eq nat i i
                      by (refl_equal . .)
eq nat i i
eq nat (minus i O) i
          end of h1
          (h2) 
             by (minus_s_s . . .)
eq nat (minus (s k i) (s k O)) (minus i O)
          end of h2
          by (eq_ind_r . . . h1 . h2)
          we proved eq nat (minus (s k i) (s k O)) i
       we proved ∀k:K.∀i:nat.(eq nat (minus (s k i) (s k O)) i)