-nat).(\lambda (H1: (getl n e1 e2)).((match k in K return (\lambda (k0:
-K).((clear (CHead c0 k0 t) (CHead e1 (Bind b) v)) \to (getl (S n) (CHead c0
-k0 t) e2))) with [(Bind b0) \Rightarrow (\lambda (H2: (clear (CHead c0 (Bind
-b0) t) (CHead e1 (Bind b) v))).(let H3 \def (f_equal C C (\lambda (e:
-C).(match e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow e1 |
-(CHead c _ _) \Rightarrow c])) (CHead e1 (Bind b) v) (CHead c0 (Bind b0) t)
-(clear_gen_bind b0 c0 (CHead e1 (Bind b) v) t H2)) in ((let H4 \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 e1
+nat).(\lambda (H1: (getl n e1 e2)).(K_ind (\lambda (k0: K).((clear (CHead c0
+k0 t) (CHead e1 (Bind b) v)) \to (getl (S n) (CHead c0 k0 t) e2))) (\lambda
+(b0: B).(\lambda (H2: (clear (CHead c0 (Bind b0) t) (CHead e1 (Bind b)
+v))).(let H3 \def (f_equal C C (\lambda (e: C).(match e in C return (\lambda
+(_: C).C) with [(CSort _) \Rightarrow e1 | (CHead c1 _ _) \Rightarrow c1]))
+(CHead e1 (Bind b) v) (CHead c0 (Bind b0) t) (clear_gen_bind b0 c0 (CHead e1
+(Bind b) v) t H2)) in ((let H4 \def (f_equal C B (\lambda (e: C).(match e in
+C return (\lambda (_: C).B) with [(CSort _) \Rightarrow b | (CHead _ k0 _)
+\Rightarrow (match k0 in K return (\lambda (_: K).B) with [(Bind b1)
+\Rightarrow b1 | (Flat _) \Rightarrow b])])) (CHead e1 (Bind b) v) (CHead c0
+(Bind b0) t) (clear_gen_bind b0 c0 (CHead e1 (Bind b) v) t H2)) in ((let H5
+\def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T)
+with [(CSort _) \Rightarrow v | (CHead _ _ t0) \Rightarrow t0])) (CHead e1