DEFINITION s()
TYPE =
       K→nat→nat
BODY =
λk:K.λi:nat.<λk1:K.nat> CASE k OF Bind ⇒S i | Flat ⇒i