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