-T).(match k in K return (\lambda (k0: K).(clear (CHead (CSort n) k0 u1)
-(CHead (CTail k0 u1 c2) (Bind b) u2))) with [(Bind b0) \Rightarrow
-(clear_gen_sort (CHead c2 (Bind b) u2) n H (clear (CHead (CSort n) (Bind b0)
-u1) (CHead (CTail (Bind b0) u1 c2) (Bind b) u2))) | (Flat f) \Rightarrow
-(clear_gen_sort (CHead c2 (Bind b) u2) n H (clear (CHead (CSort n) (Flat f)
-u1) (CHead (CTail (Flat f) u1 c2) (Bind b) u2)))]))))))) (\lambda (c:
-C).(\lambda (H: ((\forall (c2: C).(\forall (u2: T).((clear c (CHead c2 (Bind
-b) u2)) \to (\forall (k: K).(\forall (u1: T).(clear (CTail k u1 c) (CHead
-(CTail k u1 c2) (Bind b) u2))))))))).(\lambda (k: K).(\lambda (t: T).(\lambda
-(c2: C).(\lambda (u2: T).(\lambda (H0: (clear (CHead c k t) (CHead c2 (Bind
-b) u2))).(\lambda (k0: K).(\lambda (u1: T).((match k in K return (\lambda
-(k1: K).((clear (CHead c k1 t) (CHead c2 (Bind b) u2)) \to (clear (CHead
-(CTail k0 u1 c) k1 t) (CHead (CTail k0 u1 c2) (Bind b) u2)))) with [(Bind b0)
-\Rightarrow (\lambda (H1: (clear (CHead c (Bind b0) t) (CHead c2 (Bind b)
-u2))).(let H2 \def (f_equal C C (\lambda (e: C).(match e in C return (\lambda
-(_: C).C) with [(CSort _) \Rightarrow c2 | (CHead c _ _) \Rightarrow c]))
-(CHead c2 (Bind b) u2) (CHead c (Bind b0) t) (clear_gen_bind b0 c (CHead c2
-(Bind b) u2) t H1)) in ((let H3 \def (f_equal C B (\lambda (e: C).(match e in
-C return (\lambda (_: C).B) with [(CSort _) \Rightarrow b | (CHead _ k _)
-\Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b)
-\Rightarrow b | (Flat _) \Rightarrow b])])) (CHead c2 (Bind b) u2) (CHead c
-(Bind b0) t) (clear_gen_bind b0 c (CHead c2 (Bind b) u2) t H1)) in ((let H4
-\def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T)
-with [(CSort _) \Rightarrow u2 | (CHead _ _ t) \Rightarrow t])) (CHead c2
+T).(K_ind (\lambda (k0: K).(clear (CHead (CSort n) k0 u1) (CHead (CTail k0 u1
+c2) (Bind b) u2))) (\lambda (b0: B).(clear_gen_sort (CHead c2 (Bind b) u2) n
+H (clear (CHead (CSort n) (Bind b0) u1) (CHead (CTail (Bind b0) u1 c2) (Bind
+b) u2)))) (\lambda (f: F).(clear_gen_sort (CHead c2 (Bind b) u2) n H (clear
+(CHead (CSort n) (Flat f) u1) (CHead (CTail (Flat f) u1 c2) (Bind b) u2))))
+k))))))) (\lambda (c: C).(\lambda (H: ((\forall (c2: C).(\forall (u2:
+T).((clear c (CHead c2 (Bind b) u2)) \to (\forall (k: K).(\forall (u1:
+T).(clear (CTail k u1 c) (CHead (CTail k u1 c2) (Bind b) u2))))))))).(\lambda
+(k: K).(\lambda (t: T).(\lambda (c2: C).(\lambda (u2: T).(\lambda (H0: (clear
+(CHead c k t) (CHead c2 (Bind b) u2))).(\lambda (k0: K).(\lambda (u1:
+T).(K_ind (\lambda (k1: K).((clear (CHead c k1 t) (CHead c2 (Bind b) u2)) \to
+(clear (CHead (CTail k0 u1 c) k1 t) (CHead (CTail k0 u1 c2) (Bind b) u2))))
+(\lambda (b0: B).(\lambda (H1: (clear (CHead c (Bind b0) t) (CHead c2 (Bind
+b) u2))).(let H2 \def (f_equal C C (\lambda (e: C).(match e in C return
+(\lambda (_: C).C) with [(CSort _) \Rightarrow c2 | (CHead c0 _ _)
+\Rightarrow c0])) (CHead c2 (Bind b) u2) (CHead c (Bind b0) t)
+(clear_gen_bind b0 c (CHead c2 (Bind b) u2) t H1)) in ((let H3 \def (f_equal
+C B (\lambda (e: C).(match e in C return (\lambda (_: C).B) with [(CSort _)
+\Rightarrow b | (CHead _ k1 _) \Rightarrow (match k1 in K return (\lambda (_:
+K).B) with [(Bind b1) \Rightarrow b1 | (Flat _) \Rightarrow b])])) (CHead c2