\forall (P: ((TList \to Prop))).(((\forall (n: nat).((\lambda (P0: ((TList
\to Prop))).(\lambda (n0: nat).(\forall (ts: TList).((eq nat (tslen ts) n0)
\to (P0 ts))))) P n))) \to (\forall (ts: TList).(P ts)))
\forall (P: ((TList \to Prop))).(((\forall (n: nat).((\lambda (P0: ((TList
\to Prop))).(\lambda (n0: nat).(\forall (ts: TList).((eq nat (tslen ts) n0)
\to (P0 ts))))) P n))) \to (\forall (ts: TList).(P ts)))