DEFINITION tslen()
TYPE =
TList
→
nat
BODY =
Show proof