DEFINITION fweight()
TYPE =
C
→
T
→
nat
BODY =
Show proof