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