DEFINITION T_rect()
TYPE =
       ΠP:T
                →(Type:91437:cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/T_rect.con)
         .Π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