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