-let rec TApp (ts: TList) on ts: T \to TList \def \lambda (v: T).(match ts
-with [TNil \Rightarrow (TCons v TNil) | (TCons t ts0) \Rightarrow (let TMP_1
-\def (TApp ts0 v) in (TCons t TMP_1))]).
+rec definition TApp (ts: TList) on ts: T \to TList \def \lambda (v: T).(match
+ts with [TNil \Rightarrow (TCons v TNil) | (TCons t ts0) \Rightarrow (TCons t
+(TApp ts0 v))]).