DEFINITION lweight()
TYPE =
       A→nat
BODY =
FIXlweight{
         lweight:A→nat
         :=λa:A
           .<λa1:A.nat>
             CASE a OF
               ASort  ⇒O
             | AHead a1 a2⇒S (plus (lweight a1) (lweight a2))
         }