DEFINITION tcons_tapp_ex()
TYPE =
       ∀ts1:TList
         .∀t1:T
           .ex2_2
             TList
             T
             λts2:TList.λt2:T.eq TList (TCons t1 ts1) (TApp ts2 t2)
             λts2:TList.λ:T.eq nat (tslen ts1) (tslen ts2)
BODY =
       assume ts1: TList
          we proceed by induction on ts1 to prove 
             ∀t1:T
               .ex2_2
                 TList
                 T
                 λts2:TList.λt2:T.eq TList (TCons t1 ts1) (TApp ts2 t2)
                 λts2:TList.λ:T.eq nat (tslen ts1) (tslen ts2)
             case TNil : ⇒
                the thesis becomes 
                ∀t1:T
                  .ex2_2
                    TList
                    T
                    λts2:TList.λt2:T.eq TList (TCons t1 TNil) (TApp ts2 t2)
                    λts2:TList.λ:T.eq nat (tslen TNil) (tslen ts2)
                   assume t1: T
                      (h1) 
                         by (refl_equal . .)
                         we proved eq TList (TApp TNil t1) (TApp TNil t1)
eq TList (TCons t1 TNil) (TApp TNil t1)
                      end of h1
                      (h2) 
                         by (refl_equal . .)
                         we proved eq nat (tslen TNil) (tslen TNil)
eq nat O (tslen TNil)
                      end of h2
                      by (ex2_2_intro . . . . . . h1 h2)
                      we proved 
                         ex2_2
                           TList
                           T
                           λts2:TList.λt2:T.eq TList (TCons t1 TNil) (TApp ts2 t2)
                           λts2:TList.λ:T.eq nat O (tslen ts2)
                      that is equivalent to 
                         ex2_2
                           TList
                           T
                           λts2:TList.λt2:T.eq TList (TCons t1 TNil) (TApp ts2 t2)
                           λts2:TList.λ:T.eq nat (tslen TNil) (tslen ts2)

                      ∀t1:T
                        .ex2_2
                          TList
                          T
                          λts2:TList.λt2:T.eq TList (TCons t1 TNil) (TApp ts2 t2)
                          λts2:TList.λ:T.eq nat (tslen TNil) (tslen ts2)
             case TCons : t:T t0:TList ⇒
                the thesis becomes 
                ∀t1:T
                  .ex2_2
                    TList
                    T
                    λts2:TList.λt2:T.eq TList (TCons t1 (TCons t t0)) (TApp ts2 t2)
                    λts2:TList.λ:T.eq nat (S (tslen t0)) (tslen ts2)
                (H) by induction hypothesis we know 
                   ∀t1:T
                     .ex2_2
                       TList
                       T
                       λts2:TList.λt2:T.eq TList (TCons t1 t0) (TApp ts2 t2)
                       λts2:TList.λ:T.eq nat (tslen t0) (tslen ts2)
                   assume t1: T
                      (H_x) 
                         by (H .)

                            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
                      (H0) consider H_x
                      we proceed by induction on H0 to prove 
                         ex2_2
                           TList
                           T
                           λts2:TList.λt2:T.eq TList (TCons t1 (TCons t t0)) (TApp ts2 t2)
                           λts2:TList.λ:T.eq nat (S (tslen t0)) (tslen ts2)
                         case ex2_2_intro : x0:TList x1:T H1:eq TList (TCons t t0) (TApp x0 x1) H2:eq nat (tslen t0) (tslen x0) ⇒
                            the thesis becomes 
                            ex2_2
                              TList
                              T
                              λts2:TList.λt3:T.eq TList (TCons t1 (TCons t t0)) (TApp ts2 t3)
                              λts2:TList.λ:T.eq nat (S (tslen t0)) (tslen ts2)
                               (h1) 
                                  by (refl_equal . .)
                                  we proved eq TList (TApp (TCons t1 x0) x1) (TApp (TCons t1 x0) x1)
eq TList (TCons t1 (TApp x0 x1)) (TApp (TCons t1 x0) x1)
                               end of h1
                               (h2) 
                                  by (refl_equal . .)
                                  we proved eq nat (tslen (TCons t1 x0)) (tslen (TCons t1 x0))
eq nat (S (tslen x0)) (tslen (TCons t1 x0))
                               end of h2
                               by (ex2_2_intro . . . . . . h1 h2)
                               we proved 
                                  ex2_2
                                    TList
                                    T
                                    λts2:TList.λt2:T.eq TList (TCons t1 (TApp x0 x1)) (TApp ts2 t2)
                                    λts2:TList.λ:T.eq nat (S (tslen x0)) (tslen ts2)
                               by (eq_ind_r . . . previous . H2)
                               we proved 
                                  ex2_2
                                    TList
                                    T
                                    λts2:TList.λt2:T.eq TList (TCons t1 (TApp x0 x1)) (TApp ts2 t2)
                                    λts2:TList.λ:T.eq nat (S (tslen t0)) (tslen ts2)
                               by (eq_ind_r . . . previous . H1)

                                  ex2_2
                                    TList
                                    T
                                    λts2:TList.λt3:T.eq TList (TCons t1 (TCons t t0)) (TApp ts2 t3)
                                    λts2:TList.λ:T.eq nat (S (tslen t0)) (tslen ts2)
                      we proved 
                         ex2_2
                           TList
                           T
                           λts2:TList.λt2:T.eq TList (TCons t1 (TCons t t0)) (TApp ts2 t2)
                           λts2:TList.λ:T.eq nat (S (tslen t0)) (tslen ts2)
                      that is equivalent to 
                         ex2_2
                           TList
                           T
                           λts2:TList.λt2:T.eq TList (TCons t1 (TCons t t0)) (TApp ts2 t2)
                           λts2:TList.λ:T.eq nat (tslen (TCons t t0)) (tslen ts2)

                      ∀t1:T
                        .ex2_2
                          TList
                          T
                          λts2:TList.λt2:T.eq TList (TCons t1 (TCons t t0)) (TApp ts2 t2)
                          λts2:TList.λ:T.eq nat (S (tslen t0)) (tslen ts2)
          we proved 
             ∀t1:T
               .ex2_2
                 TList
                 T
                 λts2:TList.λt2:T.eq TList (TCons t1 ts1) (TApp ts2 t2)
                 λts2:TList.λ:T.eq nat (tslen ts1) (tslen ts2)
       we proved 
          ∀ts1:TList
            .∀t1:T
              .ex2_2
                TList
                T
                λts2:TList.λt2:T.eq TList (TCons t1 ts1) (TApp ts2 t2)
                λts2:TList.λ:T.eq nat (tslen ts1) (tslen ts2)