-c0)) (\lambda (c0: C).(match c0 in C return (\lambda (c1: C).(((\forall (d:
-C).((clt d c1) \to (P d)))) \to (P c1))) with [(CSort n) \Rightarrow (\lambda
-(_: ((\forall (d: C).((clt d (CSort n)) \to (P d))))).(H n)) | (CHead c1 k t)
-\Rightarrow (\lambda (H1: ((\forall (d: C).((clt d (CHead c1 k t)) \to (P
-d))))).(let H_x \def (chead_ctail c1 t k) in (let H2 \def H_x in (ex_3_ind K
-C T (\lambda (h: K).(\lambda (d: C).(\lambda (u: T).(eq C (CHead c1 k t)
+c0)) (\lambda (c0: C).(C_ind (\lambda (c1: C).(((\forall (d: C).((clt d c1)
+\to (P d)))) \to (P c1))) (\lambda (n: nat).(\lambda (_: ((\forall (d:
+C).((clt d (CSort n)) \to (P d))))).(H n))) (\lambda (c1: C).(\lambda (_:
+((((\forall (d: C).((clt d c1) \to (P d)))) \to (P c1)))).(\lambda (k:
+K).(\lambda (t: T).(\lambda (H2: ((\forall (d: C).((clt d (CHead c1 k t)) \to
+(P d))))).(let H_x \def (chead_ctail c1 t k) in (let H3 \def H_x in (ex_3_ind
+K C T (\lambda (h: K).(\lambda (d: C).(\lambda (u: T).(eq C (CHead c1 k t)