DEFINITION tslen()
TYPE =
       TList→nat
BODY =
FIXtslen{
         tslen:TList→nat
         :=λts:TList.<λt:TList.nat> CASE ts OF TNil⇒O | TCons  ts0⇒S (tslen ts0)
         }