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