DEFINITION T_rec()
TYPE =
       ΠP:T→Set
         .Π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