DEFINITION tslt_wf_ind()
TYPE =
       ∀P:TList→Prop
         .(∀ts2:TList.(∀ts1:TList.(tslt ts1 ts2)→(P ts1))→(P ts2))→∀ts:TList.(P ts)
BODY =
       (Q) 
           assume P: TList→Prop
           assume n: nat
              assume ts: TList
              suppose : eq nat (tslen ts) n
                by (. .)
                we proved 
             suppose : eq nat (tslen ts) n
                by (. .)
                we proved 
             by (. .)
             we proved 

       end of Q
        assume P: TList→Prop
        suppose H: ∀ts2:TList.(∀ts1:TList.(lt (tslen ts1) (tslen ts2))→(P ts1))→(P ts2)
        assume ts: TList
          assume n: nat
              assume n0: nat
              suppose H0: ∀m:nat.(lt m n0)→(Q λt:TList.P t m)
                we must prove Q λt:TList.P t n0
                or equivalently ∀ts0:TList.(eq nat (tslen ts0) n0)→(P ts0)
                 assume ts0: TList
                 suppose H1: eq nat (tslen ts0) n0
                   (H2) 
                      consider H0
                      we proved ∀m:nat.(lt m n0)→(Q λt:TList.P t m)
                      that is equivalent to ∀m:nat.(lt m n0)→∀ts1:TList.(eq nat (tslen ts1) m)→(P ts1)
                      by (eq_ind_r . . . previous . H1)
∀m:nat.(lt m (tslen ts0))→∀ts1:TList.(eq nat (tslen ts1) m)→(P ts1)
                   end of H2
                    assume ts1: TList
                    suppose H3: lt (tslen ts1) (tslen ts0)
                      by (refl_equal . .)
                      we proved eq nat (tslen ts1) (tslen ts1)
                      by (H2 . H3 . previous)
                      we proved P ts1
                   we proved ∀ts1:TList.(lt (tslen ts1) (tslen ts0))→(P ts1)
                   by (H . previous)
                   we proved P ts0
                we proved ∀ts0:TList.(eq nat (tslen ts0) n0)→(P ts0)
                that is equivalent to Q λt:TList.P t n0
             we proved ∀n0:nat.(∀m:nat.(lt m n0)→(Q λt:TList.P t m))→(Q λt:TList.P t n0)
             by (lt_wf_ind . . previous)
             we proved Q λt:TList.P t n
             that is equivalent to ∀ts:TList.(eq nat (tslen ts) n)→(P ts)
          we proved ∀n:nat.∀ts:TList.(eq nat (tslen ts) n)→(P ts)
          by (tslt_wf__q_ind . previous .)
          we proved P ts
       we proved 
          ∀P:TList→Prop
            .∀ts2:TList.(∀ts1:TList.(lt (tslen ts1) (tslen ts2))→(P ts1))→(P ts2)
              →∀ts:TList.(P ts)
       that is equivalent to 
          ∀P:TList→Prop
            .(∀ts2:TList.(∀ts1:TList.(tslt ts1 ts2)→(P ts1))→(P ts2))→∀ts:TList.(P ts)