DEFINITION llt_wf__q_ind()
TYPE =
       ∀P:A→Prop
         .∀n:nat.(λP0:A→Prop.λn0:nat.∀a:A.(eq nat (lweight a) n0)→(P0 a) P n)
           →∀a:A.(P a)
BODY =
Show proof