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 =
       we must prove 
             ∀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)
       or equivalently 
             ∀P:C→Prop
               .(∀n:nat.∀c:C.(eq nat (cweight c) n)→(P c))→∀c:C.(P c)
        assume P: C→Prop
        suppose H: ∀n:nat.∀c:C.(eq nat (cweight c) n)→(P c)
        assume c: C
          by (refl_equal . .)
          we proved eq nat (cweight c) (cweight c)
          by (H . . previous)
          we proved P c
       we proved 
          ∀P:C→Prop
            .(∀n:nat.∀c:C.(eq nat (cweight c) n)→(P c))→∀c:C.(P c)
       that is equivalent to 
          ∀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)