DEFINITION tslt_wf__q_ind()
TYPE =
       ∀P:TList→Prop
         .∀n:nat
             .λP0:TList→Prop.λn0:nat.∀ts:TList.(eq nat (tslen ts) n0)→(P0 ts)
               P
               n
           →∀ts:TList.(P ts)
BODY =
Show proof