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 =
       we must prove 
             ∀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)
       or equivalently 
             ∀P:TList→Prop
               .∀n:nat.∀ts:TList.(eq nat (tslen ts) n)→(P ts)
                 →∀ts:TList.(P ts)
        assume P: TList→Prop
        suppose H: ∀n:nat.∀ts:TList.(eq nat (tslen ts) n)→(P ts)
        assume ts: TList
          by (refl_equal . .)
          we proved eq nat (tslen ts) (tslen ts)
          by (H . . previous)
          we proved P ts
       we proved 
          ∀P:TList→Prop
            .∀n:nat.∀ts:TList.(eq nat (tslen ts) n)→(P ts)
              →∀ts:TList.(P ts)
       that is equivalent to 
          ∀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)