DEFINITION tlt_wf__q_ind()
TYPE =
       ∀P:T→Prop
         .∀n:nat.(λP0:T→Prop.λn0:nat.∀t:T.(eq nat (weight t) n0)→(P0 t) P n)
           →∀t:T.(P t)
BODY =
       we must prove 
             ∀P:T→Prop
               .∀n:nat.(λP0:T→Prop.λn0:nat.∀t:T.(eq nat (weight t) n0)→(P0 t) P n)
                 →∀t:T.(P t)
       or equivalently 
             ∀P:T→Prop
               .(∀n:nat.∀t:T.(eq nat (weight t) n)→(P t))→∀t:T.(P t)
        assume P: T→Prop
        suppose H: ∀n:nat.∀t:T.(eq nat (weight t) n)→(P t)
        assume t: T
          by (refl_equal . .)
          we proved eq nat (weight t) (weight t)
          by (H . . previous)
          we proved P t
       we proved 
          ∀P:T→Prop
            .(∀n:nat.∀t:T.(eq nat (weight t) n)→(P t))→∀t:T.(P t)
       that is equivalent to 
          ∀P:T→Prop
            .∀n:nat.(λP0:T→Prop.λn0:nat.∀t:T.(eq nat (weight t) n0)→(P0 t) P n)
              →∀t:T.(P t)