DEFINITION clt_wf__q_ind()
TYPE =
       ∀P:C→Prop
         .∀n:nat.(λP0:C→Prop.λn0:nat.∀c:C.(eq nat (cweight c) n0)→(P0 c) P n)
           →∀c:C.(P c)
BODY =
Show proof