- \lambda (c: C).(let TMP_4 \def (\lambda (c0: C).(\forall (t: T).(\forall (k:
-K).(let TMP_3 \def (\lambda (h: K).(\lambda (d: C).(\lambda (u: T).(let TMP_1
-\def (CHead c0 k t) in (let TMP_2 \def (CTail h u d) in (eq C TMP_1
-TMP_2)))))) in (ex_3 K C T TMP_3))))) in (let TMP_13 \def (\lambda (n:
-nat).(\lambda (t: T).(\lambda (k: K).(let TMP_8 \def (\lambda (h: K).(\lambda
-(d: C).(\lambda (u: T).(let TMP_5 \def (CSort n) in (let TMP_6 \def (CHead
-TMP_5 k t) in (let TMP_7 \def (CTail h u d) in (eq C TMP_6 TMP_7))))))) in
-(let TMP_9 \def (CSort n) in (let TMP_10 \def (CSort n) in (let TMP_11 \def
-(CHead TMP_10 k t) in (let TMP_12 \def (refl_equal C TMP_11) in (ex_3_intro K
-C T TMP_8 k TMP_9 t TMP_12))))))))) in (let TMP_38 \def (\lambda (c0:
-C).(\lambda (H: ((\forall (t: T).(\forall (k: K).(ex_3 K C T (\lambda (h:
-K).(\lambda (d: C).(\lambda (u: T).(eq C (CHead c0 k t) (CTail h u
-d)))))))))).(\lambda (k: K).(\lambda (t: T).(\lambda (t0: T).(\lambda (k0:
-K).(let H_x \def (H t k) in (let H0 \def H_x in (let TMP_16 \def (\lambda (h:
-K).(\lambda (d: C).(\lambda (u: T).(let TMP_14 \def (CHead c0 k t) in (let
-TMP_15 \def (CTail h u d) in (eq C TMP_14 TMP_15)))))) in (let TMP_20 \def
-(\lambda (h: K).(\lambda (d: C).(\lambda (u: T).(let TMP_17 \def (CHead c0 k
-t) in (let TMP_18 \def (CHead TMP_17 k0 t0) in (let TMP_19 \def (CTail h u d)
-in (eq C TMP_18 TMP_19))))))) in (let TMP_21 \def (ex_3 K C T TMP_20) in (let
-TMP_37 \def (\lambda (x0: K).(\lambda (x1: C).(\lambda (x2: T).(\lambda (H1:
-(eq C (CHead c0 k t) (CTail x0 x2 x1))).(let TMP_22 \def (CTail x0 x2 x1) in
-(let TMP_26 \def (\lambda (c1: C).(let TMP_25 \def (\lambda (h: K).(\lambda
-(d: C).(\lambda (u: T).(let TMP_23 \def (CHead c1 k0 t0) in (let TMP_24 \def
-(CTail h u d) in (eq C TMP_23 TMP_24)))))) in (ex_3 K C T TMP_25))) in (let
-TMP_30 \def (\lambda (h: K).(\lambda (d: C).(\lambda (u: T).(let TMP_27 \def
-(CTail x0 x2 x1) in (let TMP_28 \def (CHead TMP_27 k0 t0) in (let TMP_29 \def
-(CTail h u d) in (eq C TMP_28 TMP_29))))))) in (let TMP_31 \def (CHead x1 k0
-t0) in (let TMP_32 \def (CTail x0 x2 x1) in (let TMP_33 \def (CHead TMP_32 k0
-t0) in (let TMP_34 \def (refl_equal C TMP_33) in (let TMP_35 \def (ex_3_intro
-K C T TMP_30 x0 TMP_31 x2 TMP_34) in (let TMP_36 \def (CHead c0 k t) in
-(eq_ind_r C TMP_22 TMP_26 TMP_35 TMP_36 H1)))))))))))))) in (ex_3_ind K C T
-TMP_16 TMP_21 TMP_37 H0))))))))))))) in (C_ind TMP_4 TMP_13 TMP_38 c)))).
+ \lambda (c: C).(C_ind (\lambda (c0: C).(\forall (t: T).(\forall (k: K).(ex_3
+K C T (\lambda (h: K).(\lambda (d: C).(\lambda (u: T).(eq C (CHead c0 k t)
+(CTail h u d))))))))) (\lambda (n: nat).(\lambda (t: T).(\lambda (k:
+K).(ex_3_intro K C T (\lambda (h: K).(\lambda (d: C).(\lambda (u: T).(eq C
+(CHead (CSort n) k t) (CTail h u d))))) k (CSort n) t (refl_equal C (CHead
+(CSort n) k t)))))) (\lambda (c0: C).(\lambda (H: ((\forall (t: T).(\forall
+(k: K).(ex_3 K C T (\lambda (h: K).(\lambda (d: C).(\lambda (u: T).(eq C
+(CHead c0 k t) (CTail h u d)))))))))).(\lambda (k: K).(\lambda (t:
+T).(\lambda (t0: T).(\lambda (k0: K).(let H_x \def (H t k) in (let H0 \def
+H_x in (ex_3_ind K C T (\lambda (h: K).(\lambda (d: C).(\lambda (u: T).(eq C
+(CHead c0 k t) (CTail h u d))))) (ex_3 K C T (\lambda (h: K).(\lambda (d:
+C).(\lambda (u: T).(eq C (CHead (CHead c0 k t) k0 t0) (CTail h u d))))))
+(\lambda (x0: K).(\lambda (x1: C).(\lambda (x2: T).(\lambda (H1: (eq C (CHead
+c0 k t) (CTail x0 x2 x1))).(eq_ind_r C (CTail x0 x2 x1) (\lambda (c1:
+C).(ex_3 K C T (\lambda (h: K).(\lambda (d: C).(\lambda (u: T).(eq C (CHead
+c1 k0 t0) (CTail h u d))))))) (ex_3_intro K C T (\lambda (h: K).(\lambda (d:
+C).(\lambda (u: T).(eq C (CHead (CTail x0 x2 x1) k0 t0) (CTail h u d))))) x0
+(CHead x1 k0 t0) x2 (refl_equal C (CHead (CTail x0 x2 x1) k0 t0))) (CHead c0
+k t) H1))))) H0))))))))) c).