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