DEFINITION tslt()
TYPE =
       TList→TList→Prop
BODY =
λts1:TList.λts2:TList.lt (tslen ts1) (tslen ts2)