DEFINITION lweight()
TYPE =
       A→nat
BODY =
Show proof