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