DEFINITION s_arith1()
TYPE =
       ∀b:B.∀i:nat.(eq nat (minus (s (Bind b) i) (S O)) i)
BODY =
        assume : B
        assume i: nat
          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
          we proved eq nat (minus i O) i
          that is equivalent to eq nat (minus (s (Bind __2) i) (S O)) i
       we proved B→∀i:nat.(eq nat (minus (s (Bind __2) i) (S O)) i)