Fixpoint weight_map [f:nat->nat; t:T] : nat := Cases t of
| (TSort n) => (0)
- | (TBRef n) => (f n)
+ | (TLRef n) => (f n)
| (TTail (Bind Abbr) u t) =>
(S (plus (weight_map f u) (weight_map (wadd f (S (weight_map f u))) t)))
| (TTail (Bind _) u t) =>