DEFINITION s_inc()
TYPE =
       ∀k:K.∀i:nat.(le i (s k i))
BODY =
Show proof