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