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 =
Show proof