DEFINITION TList_ind()
TYPE =
       ∀P:TList→Prop
         .P TNil
           →(∀t:T.∀t1:TList.(P t1)→(P (TCons t t1)))→∀t:TList.(P t)
BODY =
        assume P: TList→Prop
        suppose H: P TNil
        suppose H1: ∀t:T.∀t1:TList.(P t1)→(P (TCons t t1))
          (aux) by well-founded reasoning we prove ∀t:TList.(P t)
          assume t: TList
             by cases on t we prove P t
                case TNil ⇒
                   the thesis becomes the hypothesis H
                case TCons t1:T t2:TList ⇒
                   the thesis becomes P (TCons t1 t2)
                   by (aux .)
                   we proved P t2
                   by (H1 . . previous)
P (TCons t1 t2)
             we proved P t
∀t:TList.(P t)
          done
          consider aux
          we proved ∀t:TList.(P t)
       we proved 
          ∀P:TList→Prop
            .P TNil
              →(∀t:T.∀t1:TList.(P t1)→(P (TCons t t1)))→∀t:TList.(P t)