DEFINITION TList_rec()
TYPE =
       ΠP:TList→Set
         .P TNil
           →(Πt:T.Πt1:TList.(P t1)→(P (TCons t t1))
                →Πt:TList.(P t))
BODY =
Show proof