DEFINITION weight_map()
TYPE =
       (nat→nat)→T→nat
BODY =
Show proof