-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.
+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))].