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