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