DEFINITION tslt_wf_ind()
TYPE =
       ∀P:TList→Prop
         .(∀ts2:TList.(∀ts1:TList.(tslt ts1 ts2)→(P ts1))→(P ts2))→∀ts:TList.(P ts)
BODY =
Show proof