-let rec CTail (k: K) (t: T) (c: C) on c: C \def match c with [(CSort n)
-\Rightarrow (let TMP_2 \def (CSort n) in (CHead TMP_2 k t)) | (CHead d h u)
-\Rightarrow (let TMP_1 \def (CTail k t d) in (CHead TMP_1 h u))].
+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)].