DEFINITION s_arith1()
TYPE =
       ∀b:B.∀i:nat.(eq nat (minus (s (Bind b) i) (S O)) i)
BODY =
Show proof