DEFINITION cbk()
TYPE =
       C→nat
BODY =
FIXcbk{
         cbk:C→nat
         :=λc:C.<λc1:C.nat> CASE c OF CSort m⇒m | CHead c0  ⇒cbk c0
         }