-(Flat f) u) (\lambda (c: C).(clear x c)) P (\lambda (y: C).(\lambda (H0:
-(clear x y)).(clear_ind (\lambda (_: C).(\lambda (c0: C).((eq C c0 (CHead e
-(Flat f) u)) \to P))) (\lambda (b: B).(\lambda (e0: C).(\lambda (u0:
-T).(\lambda (H1: (eq C (CHead e0 (Bind b) u0) (CHead e (Flat f) u))).(let H2
-\def (eq_ind C (CHead e0 (Bind b) u0) (\lambda (ee: C).(match ee in C return
-(\lambda (_: C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k _)
-\Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind _)
-\Rightarrow True | (Flat _) \Rightarrow False])])) I (CHead e (Flat f) u) H1)
-in (False_ind P H2)))))) (\lambda (e0: C).(\lambda (c: C).(\lambda (H1:
-(clear e0 c)).(\lambda (H2: (((eq C c (CHead e (Flat f) u)) \to P))).(\lambda
-(_: F).(\lambda (_: T).(\lambda (H3: (eq C c (CHead e (Flat f) u))).(let H4
-\def (eq_ind C c (\lambda (c0: C).((eq C c0 (CHead e (Flat f) u)) \to P)) H2
-(CHead e (Flat f) u) H3) in (let H5 \def (eq_ind C c (\lambda (c0: C).(clear
-e0 c0)) H1 (CHead e (Flat f) u) H3) in (H4 (refl_equal C (CHead e (Flat f)
-u)))))))))))) x y H0))) H)))))).
+(Flat f) u) (\lambda (c: C).(clear x c)) (\lambda (_: C).P) (\lambda (y:
+C).(\lambda (H0: (clear x y)).(clear_ind (\lambda (_: C).(\lambda (c0:
+C).((eq C c0 (CHead e (Flat f) u)) \to P))) (\lambda (b: B).(\lambda (e0:
+C).(\lambda (u0: T).(\lambda (H1: (eq C (CHead e0 (Bind b) u0) (CHead e (Flat
+f) u))).(let H2 \def (eq_ind C (CHead e0 (Bind b) u0) (\lambda (ee: C).(match
+ee in C return (\lambda (_: C).Prop) with [(CSort _) \Rightarrow False |
+(CHead _ k _) \Rightarrow (match k in K return (\lambda (_: K).Prop) with
+[(Bind _) \Rightarrow True | (Flat _) \Rightarrow False])])) I (CHead e (Flat
+f) u) H1) in (False_ind P H2)))))) (\lambda (e0: C).(\lambda (c: C).(\lambda
+(H1: (clear e0 c)).(\lambda (H2: (((eq C c (CHead e (Flat f) u)) \to
+P))).(\lambda (_: F).(\lambda (_: T).(\lambda (H3: (eq C c (CHead e (Flat f)
+u))).(let H4 \def (eq_ind C c (\lambda (c0: C).((eq C c0 (CHead e (Flat f)
+u)) \to P)) H2 (CHead e (Flat f) u) H3) in (let H5 \def (eq_ind C c (\lambda
+(c0: C).(clear e0 c0)) H1 (CHead e (Flat f) u) H3) in (H4 (refl_equal C
+(CHead e (Flat f) u)))))))))))) x y H0))) H)))))).