-let rec app1 (c: C) on c: T \to T \def \lambda (t: T).(match c with [(CSort
-_) \Rightarrow t | (CHead c0 k u) \Rightarrow (let TMP_1 \def (THead k u t)
-in (app1 c0 TMP_1))]).
+rec definition app1 (c: C) on c: T \to T \def \lambda (t: T).(match c with
+[(CSort _) \Rightarrow t | (CHead c0 k u) \Rightarrow (app1 c0 (THead k u
+t))]).