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 =
λP:T→Set
         .λf:Πn:nat.(P (TSort n))
           .λf1:Πn:nat.(P (TLRef n))
             .λf2:Πk:K.Πt:T.(P t)→Πt1:T.(P t1)→(P (THead k t t1))
               .FIXaux{
                 aux:Πt:T.(P t)
                 :=λt:T
                   .<P>
                     CASE t OF
                       TSort n⇒f n
                     | TLRef n⇒f1 n
                     | THead k t1 t2⇒f2 k t1 (aux t1) t2 (aux t2)
                 }