DEFINITION clt_wf_ind()
TYPE =
       ∀P:C→Prop.(∀c:C.(∀d:C.(clt d c)→(P d))→(P c))→∀c:C.(P c)
BODY =
       (Q) 
           assume P: C→Prop
           assume n: nat
              assume c: C
              suppose : eq nat (cweight c) n
                by (. .)
                we proved 
             suppose : eq nat (cweight c) n
                by (. .)
                we proved 
             by (. .)
             we proved 

       end of Q
        assume P: C→Prop
        suppose H: ∀c:C.(∀d:C.(lt (cweight d) (cweight c))→(P d))→(P c)
        assume c: C
          assume n: nat
              assume n0: nat
              suppose H0: ∀m:nat.(lt m n0)→(Q λc0:C.P c0 m)
                we must prove Q λc0:C.P c0 n0
                or equivalently ∀c0:C.(eq nat (cweight c0) n0)→(P c0)
                 assume c0: C
                 suppose H1: eq nat (cweight c0) n0
                   (H2) 
                      consider H0
                      we proved ∀m:nat.(lt m n0)→(Q λc0:C.P c0 m)
                      that is equivalent to ∀m:nat.(lt m n0)→∀c1:C.(eq nat (cweight c1) m)→(P c1)
                      by (eq_ind_r . . . previous . H1)
∀m:nat.(lt m (cweight c0))→∀c1:C.(eq nat (cweight c1) m)→(P c1)
                   end of H2
                    assume d: C
                    suppose H3: lt (cweight d) (cweight c0)
                      by (refl_equal . .)
                      we proved eq nat (cweight d) (cweight d)
                      by (H2 . H3 . previous)
                      we proved P d
                   we proved ∀d:C.(lt (cweight d) (cweight c0))→(P d)
                   by (H . previous)
                   we proved P c0
                we proved ∀c0:C.(eq nat (cweight c0) n0)→(P c0)
                that is equivalent to Q λc0:C.P c0 n0
             we proved ∀n0:nat.(∀m:nat.(lt m n0)→(Q λc0:C.P c0 m))→(Q λc0:C.P c0 n0)
             by (lt_wf_ind . . previous)
             we proved Q λc0:C.P c0 n
             that is equivalent to ∀c:C.(eq nat (cweight c) n)→(P c)
          we proved ∀n:nat.∀c:C.(eq nat (cweight c) n)→(P c)
          by (clt_wf__q_ind . previous .)
          we proved P c
       we proved 
          ∀P:C→Prop
            .∀c:C.(∀d:C.(lt (cweight d) (cweight c))→(P d))→(P c)
              →∀c:C.(P c)
       that is equivalent to 
          ∀P:C→Prop.(∀c:C.(∀d:C.(clt d c)→(P d))→(P c))→∀c:C.(P c)