DEFINITION weight_map()
TYPE =
       (nat→nat)→T→nat
BODY =
FIXweight_map{
         weight_map:(nat→nat)→T→nat
         :=λf:nat→nat
           .λt:T
             .<λt1:T.nat>
               CASE t OF
                 TSort ⇒O
               | TLRef n⇒f n
               | THead k u t0⇒
                     <λk1:K.nat>
                       CASE k OF
                         Bind b⇒
                             <λb1:B.nat>
                               CASE b OF
                                 Abbr⇒
                                     S
                                       plus
                                         weight_map f u
                                         weight_map (wadd f (S (weight_map f u))) t0
                               | Abst⇒S (plus (weight_map f u) (weight_map (wadd f O) t0))
                               | Void⇒S (plus (weight_map f u) (weight_map (wadd f O) t0))
                       | Flat ⇒S (plus (weight_map f u) (weight_map f t0))
         }