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