DEFINITION clen()
TYPE =
       C→nat
BODY =
FIXclen{
         clen:C→nat
         :=λc:C.<λc1:C.nat> CASE c OF CSort ⇒O | CHead c0 k ⇒s k (clen c0)
         }