DEFINITION TList_ind()
TYPE =
       ∀P:TList→Prop
         .P TNil
           →(∀t:T.∀t1:TList.(P t1)→(P (TCons t t1)))→∀t:TList.(P t)
BODY =
Show proof