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 =
Show proof