DEFINITION llt_wf_ind()
TYPE =
       ∀P:A→Prop.(∀a2:A.(∀a1:A.(llt a1 a2)→(P a1))→(P a2))→∀a:A.(P a)
BODY =
       (Q) 
           assume P: A→Prop
           assume n: nat
              assume a: A
              suppose : eq nat (lweight a) n
                by (. .)
                we proved 
             suppose : eq nat (lweight a) n
                by (. .)
                we proved 
             by (. .)
             we proved 

       end of Q
        assume P: A→Prop
        suppose H: ∀a2:A.(∀a1:A.(lt (lweight a1) (lweight a2))→(P a1))→(P a2)
        assume a: A
          assume n: nat
              assume n0: nat
              suppose H0: ∀m:nat.(lt m n0)→(Q λa0:A.P a0 m)
                we must prove Q λa0:A.P a0 n0
                or equivalently ∀a0:A.(eq nat (lweight a0) n0)→(P a0)
                 assume a0: A
                 suppose H1: eq nat (lweight a0) n0
                   (H2) 
                      consider H0
                      we proved ∀m:nat.(lt m n0)→(Q λa0:A.P a0 m)
                      that is equivalent to ∀m:nat.(lt m n0)→∀a1:A.(eq nat (lweight a1) m)→(P a1)
                      by (eq_ind_r . . . previous . H1)
∀m:nat.(lt m (lweight a0))→∀a1:A.(eq nat (lweight a1) m)→(P a1)
                   end of H2
                    assume a1: A
                    suppose H3: lt (lweight a1) (lweight a0)
                      by (refl_equal . .)
                      we proved eq nat (lweight a1) (lweight a1)
                      by (H2 . H3 . previous)
                      we proved P a1
                   we proved ∀a1:A.(lt (lweight a1) (lweight a0))→(P a1)
                   by (H . previous)
                   we proved P a0
                we proved ∀a0:A.(eq nat (lweight a0) n0)→(P a0)
                that is equivalent to Q λa0:A.P a0 n0
             we proved ∀n0:nat.(∀m:nat.(lt m n0)→(Q λa0:A.P a0 m))→(Q λa0:A.P a0 n0)
             by (lt_wf_ind . . previous)
             we proved Q λa0:A.P a0 n
             that is equivalent to ∀a:A.(eq nat (lweight a) n)→(P a)
          we proved ∀n:nat.∀a:A.(eq nat (lweight a) n)→(P a)
          by (llt_wf__q_ind . previous .)
          we proved P a
       we proved 
          ∀P:A→Prop
            .∀a2:A.(∀a1:A.(lt (lweight a1) (lweight a2))→(P a1))→(P a2)
              →∀a:A.(P a)
       that is equivalent to ∀P:A→Prop.(∀a2:A.(∀a1:A.(llt a1 a2)→(P a1))→(P a2))→∀a:A.(P a)