DEFINITION weight()
TYPE =
       T→nat
BODY =
weight_map λ:nat.O