-inductive TList: Set \def
-| TNil: TList
-| TCons: T \to (TList \to TList).
-
-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.
-