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 =
Show proof