(CHead c0 _ _) \Rightarrow (cbk c0)].
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))]).
+_) \Rightarrow t | (CHead c0 k u) \Rightarrow (app1 c0 (THead k u t))]).