| (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) =>
| (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) =>