DEFINITION cweight()
TYPE =
       C→nat
BODY =
FIXcweight{
         cweight:C→nat
         :=λc:C
           .<λc1:C.nat>
             CASE c OF
               CSort ⇒O
             | CHead c0  t⇒plus (cweight c0) (tweight t)
         }