DEFINITION tlist_ind_rev()
TYPE =
       ∀P:TList→Prop
         .P TNil
           →(∀ts:TList.∀t:T.(P ts)→(P (TApp ts t)))→∀ts:TList.(P ts)
BODY =
Show proof