-definition CTail:
- K \to (T \to (C \to C))
-\def
- let rec CTail (k: K) (t: T) (c: C) on c: C \def (match c with [(CSort n)
-\Rightarrow (CHead (CSort n) k t) | (CHead d h u) \Rightarrow (CHead (CTail k
-t d) h u)]) in CTail.
+rec definition CTail (k: K) (t: T) (c: C) on c: C \def match c with [(CSort
+n) \Rightarrow (CHead (CSort n) k t) | (CHead d h u) \Rightarrow (CHead
+(CTail k t d) h u)].