DEFINITION s_arith0()
TYPE =
∀
k:
K
.
∀
i:
nat
.(
eq
nat
(
minus
(
s
k i) (
s
k
O
)) i)
BODY =
Show proof