DEFINITION cnt_ind()
TYPE =
       ∀P:T→Prop
         .∀n:nat.(P (TSort n))
           →(∀t:T.(cnt t)→(P t)→∀k:K.∀t1:T.(P (THead k t1 t))
                →∀t:T.(cnt t)→(P t))
BODY =
        assume P: T→Prop
        suppose H: ∀n:nat.(P (TSort n))
        suppose H1: ∀t:T.(cnt t)→(P t)→∀k:K.∀t1:T.(P (THead k t1 t))
          (aux) by well-founded reasoning we prove ∀t:T.(cnt t)→(P t)
           assume t: T
           suppose H2: cnt t
             by cases on H2 we prove P t
                case cnt_sort n:nat ⇒
                   the thesis becomes P (TSort n)
                   by (H .)
P (TSort n)
                case cnt_head t1:T H3:cnt t1 k:K t2:T ⇒
                   the thesis becomes P (THead k t2 t1)
                   by (aux . H3)
                   we proved P t1
                   by (H1 . H3 previous . .)
P (THead k t2 t1)
             we proved P t
∀t:T.(cnt t)→(P t)
          done
          consider aux
          we proved ∀t:T.(cnt t)→(P t)
       we proved 
          ∀P:T→Prop
            .∀n:nat.(P (TSort n))
              →(∀t:T.(cnt t)→(P t)→∀k:K.∀t1:T.(P (THead k t1 t))
                   →∀t:T.(cnt t)→(P t))