DEFINITION flt_wf_ind()
TYPE =
       ∀P:C→T→Prop
         .(∀c2:C.∀t2:T.(∀c1:C.∀t1:T.(flt c1 t1 c2 t2)→(P c1 t1))→(P c2 t2))→∀c:C.∀t:T.(P c t)
BODY =
       (Q) 
           assume P: C→T→Prop
           assume n: nat
              assume c: C
              assume t: T
              suppose : eq nat (fweight c t) n
                by (. . .)
                we proved 
              assume t: T
              suppose : eq nat (fweight c t) n
                by (. . .)
                we proved 
             suppose : eq nat (fweight c t) n
                by (. . .)
                we proved 
             by (. . .)
             we proved 

       end of Q
        assume P: C→T→Prop
        suppose H: ∀c2:C.∀t2:T.(∀c1:C.∀t1:T.(flt c1 t1 c2 t2)→(P c1 t1))→(P c2 t2)
        assume c: C
        assume t: T
          assume n: nat
              assume n0: nat
              suppose H0: ∀m:nat.(lt m n0)→(Q P m)
                we must prove Q P n0
                or equivalently ∀c0:C.∀t0:T.(eq nat (fweight c0 t0) n0)→(P c0 t0)
                 assume c0: C
                 assume t0: T
                 suppose H1: eq nat (fweight c0 t0) n0
                   (H2) 
                      consider H0
                      we proved ∀m:nat.(lt m n0)→(Q P m)
                      that is equivalent to ∀m:nat.(lt m n0)→∀c1:C.∀t1:T.(eq nat (fweight c1 t1) m)→(P c1 t1)
                      by (eq_ind_r . . . previous . H1)

                         ∀m:nat.(lt m (fweight c0 t0))→∀c1:C.∀t1:T.(eq nat (fweight c1 t1) m)→(P c1 t1)
                   end of H2
                    assume c1: C
                    assume t1: T
                    suppose H3: flt c1 t1 c0 t0
                      (h1) 
                         consider H3
                         we proved flt c1 t1 c0 t0
lt (fweight c1 t1) (fweight c0 t0)
                      end of h1
                      (h2) 
                         by (refl_equal . .)
eq nat (fweight c1 t1) (fweight c1 t1)
                      end of h2
                      by (H2 . h1 . . h2)
                      we proved P c1 t1
                   we proved ∀c1:C.∀t1:T.(flt c1 t1 c0 t0)→(P c1 t1)
                   by (H . . previous)
                   we proved P c0 t0
                we proved ∀c0:C.∀t0:T.(eq nat (fweight c0 t0) n0)→(P c0 t0)
                that is equivalent to Q P n0
             we proved ∀n0:nat.(∀m:nat.(lt m n0)→(Q P m))→(Q P n0)
             by (lt_wf_ind . . previous)
             we proved Q P n
             that is equivalent to ∀c:C.∀t:T.(eq nat (fweight c t) n)→(P c t)
          we proved ∀n:nat.∀c:C.∀t:T.(eq nat (fweight c t) n)→(P c t)
          by (flt_wf__q_ind . previous . .)
          we proved P c t
       we proved 
          ∀P:C→T→Prop
            .(∀c2:C.∀t2:T.(∀c1:C.∀t1:T.(flt c1 t1 c2 t2)→(P c1 t1))→(P c2 t2))→∀c:C.∀t:T.(P c t)