\forall (ts1: TList).(\forall (t1: T).(ex2_2 TList T (\lambda (ts2:
TList).(\lambda (t2: T).(eq TList (TCons t1 ts1) (TApp ts2 t2)))) (\lambda
(ts2: TList).(\lambda (_: T).(eq nat (tslen ts1) (tslen ts2))))))
\forall (ts1: TList).(\forall (t1: T).(ex2_2 TList T (\lambda (ts2:
TList).(\lambda (t2: T).(eq TList (TCons t1 ts1) (TApp ts2 t2)))) (\lambda
(ts2: TList).(\lambda (_: T).(eq nat (tslen ts1) (tslen ts2))))))