DEFINITION tlt_wf_ind()
TYPE =
       ∀P:T→Prop.(∀t:T.(∀v:T.(tlt v t)→(P v))→(P t))→∀t:T.(P t)
BODY =
       (Q) 
           assume P: T→Prop
           assume n: nat
              assume t: T
              suppose : eq nat (weight t) n
                by (. .)
                we proved 
             suppose : eq nat (weight t) n
                by (. .)
                we proved 
             by (. .)
             we proved 

       end of Q
        assume P: T→Prop
        suppose H: ∀t:T.(∀v:T.(lt (weight v) (weight t))→(P v))→(P t)
        assume t: T
          assume n: nat
              assume n0: nat
              suppose H0: ∀m:nat.(lt m n0)→(Q λt0:T.P t0 m)
                we must prove Q λt0:T.P t0 n0
                or equivalently ∀t0:T.(eq nat (weight t0) n0)→(P t0)
                 assume t0: T
                 suppose H1: eq nat (weight t0) n0
                   (H2) 
                      consider H0
                      we proved ∀m:nat.(lt m n0)→(Q λt0:T.P t0 m)
                      that is equivalent to ∀m:nat.(lt m n0)→∀t1:T.(eq nat (weight t1) m)→(P t1)
                      by (eq_ind_r . . . previous . H1)
∀m:nat.(lt m (weight t0))→∀t1:T.(eq nat (weight t1) m)→(P t1)
                   end of H2
                    assume v: T
                    suppose H3: lt (weight v) (weight t0)
                      by (refl_equal . .)
                      we proved eq nat (weight v) (weight v)
                      by (H2 . H3 . previous)
                      we proved P v
                   we proved ∀v:T.(lt (weight v) (weight t0))→(P v)
                   by (H . previous)
                   we proved P t0
                we proved ∀t0:T.(eq nat (weight t0) n0)→(P t0)
                that is equivalent to Q λt0:T.P t0 n0
             we proved ∀n0:nat.(∀m:nat.(lt m n0)→(Q λt0:T.P t0 m))→(Q λt0:T.P t0 n0)
             by (lt_wf_ind . . previous)
             we proved Q λt0:T.P t0 n
             that is equivalent to ∀t:T.(eq nat (weight t) n)→(P t)
          we proved ∀n:nat.∀t:T.(eq nat (weight t) n)→(P t)
          by (tlt_wf__q_ind . previous .)
          we proved P t
       we proved 
          ∀P:T→Prop
            .∀t:T.(∀v:T.(lt (weight v) (weight t))→(P v))→(P t)
              →∀t:T.(P t)
       that is equivalent to 
          ∀P:T→Prop.(∀t:T.(∀v:T.(tlt v t)→(P v))→(P t))→∀t:T.(P t)