DEFINITION tlt_wf__q_ind()
TYPE =
       ∀P:T→Prop
         .∀n:nat.(λP0:T→Prop.λn0:nat.∀t:T.(eq nat (weight t) n0)→(P0 t) P n)
           →∀t:T.(P t)
BODY =
Show proof