DEFINITION tweight()
TYPE =
       T→nat
BODY =
FIXtweight{
         tweight:T→nat
         :=λt:T
           .<λt1:T.nat>
             CASE t OF
               TSort ⇒S O
             | TLRef ⇒S O
             | THead  u t0⇒S (plus (tweight u) (tweight t0))
         }