DEFINITION TList_rect()
TYPE =
       ΠP:TList
                →(Type:124747:cic:/matita/LAMBDA-TYPES/LambdaDelta-1/tlist/defs/TList_rect.con)
         .P TNil
           →(Πt:T.Πt1:TList.(P t1)→(P (TCons t t1))
                →Πt:TList.(P t))
BODY =
λP:TList
               →(Type:124747:cic:/matita/LAMBDA-TYPES/LambdaDelta-1/tlist/defs/TList_rect.con)
         .λ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)
               }