DEFINITION tslt()
TYPE =
       TList→TList→Prop
BODY =
Show proof