-definition THeads:
- K \to (TList \to (T \to T))
-\def
- let rec THeads (k: K) (us: TList) on us: (T \to T) \def (\lambda (t:
-T).(match us with [TNil \Rightarrow t | (TCons u ul) \Rightarrow (THead k u
-(THeads k ul t))])) in THeads.
+let rec THeads (k: K) (us: TList) on us: T \to T \def \lambda (t: T).(match
+us with [TNil \Rightarrow t | (TCons u ul) \Rightarrow (let TMP_1 \def
+(THeads k ul t) in (THead k u TMP_1))]).