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 =
        assume P: TList→Prop
        suppose H: P TNil
        suppose H0: ∀ts:TList.∀t:T.(P ts)→(P (TApp ts t))
        assume ts: TList
          assume ts2: TList
             we proceed by induction on ts2 to prove (∀ts1:TList.(tslt ts1 ts2)→(P ts1))→(P ts2)
                case TNil : ⇒
                   the thesis becomes (∀ts1:TList.(tslt ts1 TNil)→(P ts1))→(P TNil)
                      suppose : ∀ts1:TList.(tslt ts1 TNil)→(P ts1)
                         consider H
(∀ts1:TList.(tslt ts1 TNil)→(P ts1))→(P TNil)
                case TCons : t:T t0:TList ⇒
                   the thesis becomes ∀H2:∀ts1:TList.(tslt ts1 (TCons t t0))→(P ts1).(P (TCons t t0))
                   () by induction hypothesis we know (∀ts1:TList.(tslt ts1 t0)→(P ts1))→(P t0)
                      suppose H2: ∀ts1:TList.(tslt ts1 (TCons t t0))→(P ts1)
                         (H_x) 
                            by (tcons_tapp_ex . .)

                               ex2_2
                                 TList
                                 T
                                 λts2:TList.λt2:T.eq TList (TCons t t0) (TApp ts2 t2)
                                 λts2:TList.λ:T.eq nat (tslen t0) (tslen ts2)
                         end of H_x
                         (H3) consider H_x
                         we proceed by induction on H3 to prove P (TCons t t0)
                            case ex2_2_intro : x0:TList x1:T H4:eq TList (TCons t t0) (TApp x0 x1) H5:eq nat (tslen t0) (tslen x0) ⇒
                               the thesis becomes P (TCons t t0)
                                  we proceed by induction on H5 to prove lt (tslen x0) (tslen (TCons t t0))
                                     case refl_equal : ⇒
                                        the thesis becomes lt (tslen t0) (tslen (TCons t t0))
                                           by (le_n .)
                                           we proved le (tslen (TCons t t0)) (tslen (TCons t t0))
lt (tslen t0) (tslen (TCons t t0))
                                  we proved lt (tslen x0) (tslen (TCons t t0))
                                  that is equivalent to tslt x0 (TCons t t0)
                                  by (H2 . previous)
                                  we proved P x0
                                  by (H0 . . previous)
                                  we proved P (TApp x0 x1)
                                  by (eq_ind_r . . . previous . H4)
P (TCons t t0)
                         we proved P (TCons t t0)
∀H2:∀ts1:TList.(tslt ts1 (TCons t t0))→(P ts1).(P (TCons t t0))
             we proved (∀ts1:TList.(tslt ts1 ts2)→(P ts1))→(P ts2)
          we proved ∀ts2:TList.(∀ts1:TList.(tslt ts1 ts2)→(P ts1))→(P ts2)
          by (tslt_wf_ind . previous .)
          we proved P ts
       we proved 
          ∀P:TList→Prop
            .P TNil
              →(∀ts:TList.∀t:T.(P ts)→(P (TApp ts t)))→∀ts:TList.(P ts)