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