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