DEFINITION TList_rec()
TYPE =
       ΠP:TList→Set
         .P TNil
           →(Πt:T.Πt1:TList.(P t1)→(P (TCons t t1))
                →Πt:TList.(P t))
BODY =
λP:TList→Set
         .λp:P TNil
           .λf:Πt:T.Πt1:TList.(P t1)→(P (TCons t t1))
             .FIXaux{
               aux:Πt:TList.(P t)
               :=λt:TList.<P> CASE t OF TNil⇒p | TCons t1 t2⇒f t1 t2 (aux t2)
               }