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 =
Show proof