-C).(\lambda (H0: (csubc g (CHead e (Bind b) u) c2)).(let H1 \def (match H0 in
-csubc return (\lambda (c: C).(\lambda (c0: C).(\lambda (_: (csubc ? c
-c0)).((eq C c (CHead e (Bind b) u)) \to ((eq C c0 c2) \to (ex2 C (\lambda
-(e2: C).(clear c2 e2)) (\lambda (e2: C).(csubc g (CHead e (Bind b) u)
-e2)))))))) with [(csubc_sort n) \Rightarrow (\lambda (H1: (eq C (CSort n)
-(CHead e (Bind b) u))).(\lambda (H2: (eq C (CSort n) c2)).((let H3 \def
-(eq_ind C (CSort n) (\lambda (e0: C).(match e0 in C return (\lambda (_:
-C).Prop) with [(CSort _) \Rightarrow True | (CHead _ _ _) \Rightarrow
-False])) I (CHead e (Bind b) u) H1) in (False_ind ((eq C (CSort n) c2) \to
-(ex2 C (\lambda (e2: C).(clear c2 e2)) (\lambda (e2: C).(csubc g (CHead e
-(Bind b) u) e2)))) H3)) H2))) | (csubc_head c0 c3 H1 k v) \Rightarrow
-(\lambda (H2: (eq C (CHead c0 k v) (CHead e (Bind b) u))).(\lambda (H3: (eq C
-(CHead c3 k v) c2)).((let H4 \def (f_equal C T (\lambda (e0: C).(match e0 in
-C return (\lambda (_: C).T) with [(CSort _) \Rightarrow v | (CHead _ _ t)
-\Rightarrow t])) (CHead c0 k v) (CHead e (Bind b) u) H2) in ((let H5 \def
-(f_equal C K (\lambda (e0: C).(match e0 in C return (\lambda (_: C).K) with
-[(CSort _) \Rightarrow k | (CHead _ k0 _) \Rightarrow k0])) (CHead c0 k v)
-(CHead e (Bind b) u) H2) in ((let H6 \def (f_equal C C (\lambda (e0:
-C).(match e0 in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c0 |
-(CHead c _ _) \Rightarrow c])) (CHead c0 k v) (CHead e (Bind b) u) H2) in
-(eq_ind C e (\lambda (c: C).((eq K k (Bind b)) \to ((eq T v u) \to ((eq C
-(CHead c3 k v) c2) \to ((csubc g c c3) \to (ex2 C (\lambda (e2: C).(clear c2
-e2)) (\lambda (e2: C).(csubc g (CHead e (Bind b) u) e2)))))))) (\lambda (H7:
-(eq K k (Bind b))).(eq_ind K (Bind b) (\lambda (k0: K).((eq T v u) \to ((eq C
-(CHead c3 k0 v) c2) \to ((csubc g e c3) \to (ex2 C (\lambda (e2: C).(clear c2
-e2)) (\lambda (e2: C).(csubc g (CHead e (Bind b) u) e2))))))) (\lambda (H8:
-(eq T v u)).(eq_ind T u (\lambda (t: T).((eq C (CHead c3 (Bind b) t) c2) \to
-((csubc g e c3) \to (ex2 C (\lambda (e2: C).(clear c2 e2)) (\lambda (e2:
-C).(csubc g (CHead e (Bind b) u) e2)))))) (\lambda (H9: (eq C (CHead c3 (Bind
-b) u) c2)).(eq_ind C (CHead c3 (Bind b) u) (\lambda (c: C).((csubc g e c3)
-\to (ex2 C (\lambda (e2: C).(clear c e2)) (\lambda (e2: C).(csubc g (CHead e
-(Bind b) u) e2))))) (\lambda (H10: (csubc g e c3)).(ex_intro2 C (\lambda (e2:
-C).(clear (CHead c3 (Bind b) u) e2)) (\lambda (e2: C).(csubc g (CHead e (Bind
-b) u) e2)) (CHead c3 (Bind b) u) (clear_bind b c3 u) (csubc_head g e c3 H10
-(Bind b) u))) c2 H9)) v (sym_eq T v u H8))) k (sym_eq K k (Bind b) H7))) c0
-(sym_eq C c0 e H6))) H5)) H4)) H3 H1))) | (csubc_abst c0 c3 H1 v a H2 w H3)
-\Rightarrow (\lambda (H4: (eq C (CHead c0 (Bind Abst) v) (CHead e (Bind b)
-u))).(\lambda (H5: (eq C (CHead c3 (Bind Abbr) w) c2)).((let H6 \def (f_equal
-C T (\lambda (e0: C).(match e0 in C return (\lambda (_: C).T) with [(CSort _)
-\Rightarrow v | (CHead _ _ t) \Rightarrow t])) (CHead c0 (Bind Abst) v)
-(CHead e (Bind b) u) H4) in ((let H7 \def (f_equal C B (\lambda (e0:
-C).(match e0 in C return (\lambda (_: C).B) with [(CSort _) \Rightarrow Abst
-| (CHead _ k _) \Rightarrow (match k in K return (\lambda (_: K).B) with
-[(Bind b0) \Rightarrow b0 | (Flat _) \Rightarrow Abst])])) (CHead c0 (Bind
-Abst) v) (CHead e (Bind b) u) H4) in ((let H8 \def (f_equal C C (\lambda (e0:
-C).(match e0 in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c0 |
-(CHead c _ _) \Rightarrow c])) (CHead c0 (Bind Abst) v) (CHead e (Bind b) u)
-H4) in (eq_ind C e (\lambda (c: C).((eq B Abst b) \to ((eq T v u) \to ((eq C
-(CHead c3 (Bind Abbr) w) c2) \to ((csubc g c c3) \to ((sc3 g (asucc g a) c v)
-\to ((sc3 g a c3 w) \to (ex2 C (\lambda (e2: C).(clear c2 e2)) (\lambda (e2:
-C).(csubc g (CHead e (Bind b) u) e2)))))))))) (\lambda (H9: (eq B Abst
-b)).(eq_ind B Abst (\lambda (b0: B).((eq T v u) \to ((eq C (CHead c3 (Bind
-Abbr) w) c2) \to ((csubc g e c3) \to ((sc3 g (asucc g a) e v) \to ((sc3 g a
-c3 w) \to (ex2 C (\lambda (e2: C).(clear c2 e2)) (\lambda (e2: C).(csubc g
-(CHead e (Bind b0) u) e2))))))))) (\lambda (H10: (eq T v u)).(eq_ind T u
-(\lambda (t: T).((eq C (CHead c3 (Bind Abbr) w) c2) \to ((csubc g e c3) \to
-((sc3 g (asucc g a) e t) \to ((sc3 g a c3 w) \to (ex2 C (\lambda (e2:
-C).(clear c2 e2)) (\lambda (e2: C).(csubc g (CHead e (Bind Abst) u)
-e2)))))))) (\lambda (H11: (eq C (CHead c3 (Bind Abbr) w) c2)).(eq_ind C
-(CHead c3 (Bind Abbr) w) (\lambda (c: C).((csubc g e c3) \to ((sc3 g (asucc g
-a) e u) \to ((sc3 g a c3 w) \to (ex2 C (\lambda (e2: C).(clear c e2))
-(\lambda (e2: C).(csubc g (CHead e (Bind Abst) u) e2))))))) (\lambda (H12:
-(csubc g e c3)).(\lambda (H13: (sc3 g (asucc g a) e u)).(\lambda (H14: (sc3 g
-a c3 w)).(ex_intro2 C (\lambda (e2: C).(clear (CHead c3 (Bind Abbr) w) e2))
-(\lambda (e2: C).(csubc g (CHead e (Bind Abst) u) e2)) (CHead c3 (Bind Abbr)
-w) (clear_bind Abbr c3 w) (csubc_abst g e c3 H12 u a H13 w H14))))) c2 H11))
-v (sym_eq T v u H10))) b H9)) c0 (sym_eq C c0 e H8))) H7)) H6)) H5 H1 H2
-H3)))]) in (H1 (refl_equal C (CHead e (Bind b) u)) (refl_equal C c2))))))))
+C).(\lambda (H0: (csubc g (CHead e (Bind b) u) c2)).(let H_x \def
+(csubc_gen_head_l g e c2 u (Bind b) H0) in (let H1 \def H_x in (or3_ind (ex2
+C (\lambda (c3: C).(eq C c2 (CHead c3 (Bind b) u))) (\lambda (c3: C).(csubc g
+e c3))) (ex5_3 C T A (\lambda (_: C).(\lambda (_: T).(\lambda (_: A).(eq K
+(Bind b) (Bind Abst))))) (\lambda (c3: C).(\lambda (w: T).(\lambda (_: A).(eq
+C c2 (CHead c3 (Bind Abbr) w))))) (\lambda (c3: C).(\lambda (_: T).(\lambda
+(_: A).(csubc g e c3)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(sc3
+g (asucc g a) e u)))) (\lambda (c3: C).(\lambda (w: T).(\lambda (a: A).(sc3 g
+a c3 w))))) (ex4_3 B C T (\lambda (b0: B).(\lambda (c3: C).(\lambda (v2:
+T).(eq C c2 (CHead c3 (Bind b0) v2))))) (\lambda (_: B).(\lambda (_:
+C).(\lambda (_: T).(eq K (Bind b) (Bind Void))))) (\lambda (b0: B).(\lambda
+(_: C).(\lambda (_: T).(not (eq B b0 Void))))) (\lambda (_: B).(\lambda (c3:
+C).(\lambda (_: T).(csubc g e c3))))) (ex2 C (\lambda (e2: C).(clear c2 e2))
+(\lambda (e2: C).(csubc g (CHead e (Bind b) u) e2))) (\lambda (H2: (ex2 C
+(\lambda (c3: C).(eq C c2 (CHead c3 (Bind b) u))) (\lambda (c3: C).(csubc g e
+c3)))).(ex2_ind C (\lambda (c3: C).(eq C c2 (CHead c3 (Bind b) u))) (\lambda
+(c3: C).(csubc g e c3)) (ex2 C (\lambda (e2: C).(clear c2 e2)) (\lambda (e2:
+C).(csubc g (CHead e (Bind b) u) e2))) (\lambda (x: C).(\lambda (H3: (eq C c2
+(CHead x (Bind b) u))).(\lambda (H4: (csubc g e x)).(eq_ind_r C (CHead x
+(Bind b) u) (\lambda (c: C).(ex2 C (\lambda (e2: C).(clear c e2)) (\lambda
+(e2: C).(csubc g (CHead e (Bind b) u) e2)))) (ex_intro2 C (\lambda (e2:
+C).(clear (CHead x (Bind b) u) e2)) (\lambda (e2: C).(csubc g (CHead e (Bind
+b) u) e2)) (CHead x (Bind b) u) (clear_bind b x u) (csubc_head g e x H4 (Bind
+b) u)) c2 H3)))) H2)) (\lambda (H2: (ex5_3 C T A (\lambda (_: C).(\lambda (_:
+T).(\lambda (_: A).(eq K (Bind b) (Bind Abst))))) (\lambda (c3: C).(\lambda
+(w: T).(\lambda (_: A).(eq C c2 (CHead c3 (Bind Abbr) w))))) (\lambda (c3:
+C).(\lambda (_: T).(\lambda (_: A).(csubc g e c3)))) (\lambda (_: C).(\lambda
+(_: T).(\lambda (a: A).(sc3 g (asucc g a) e u)))) (\lambda (c3: C).(\lambda
+(w: T).(\lambda (a: A).(sc3 g a c3 w)))))).(ex5_3_ind C T A (\lambda (_:
+C).(\lambda (_: T).(\lambda (_: A).(eq K (Bind b) (Bind Abst))))) (\lambda
+(c3: C).(\lambda (w: T).(\lambda (_: A).(eq C c2 (CHead c3 (Bind Abbr) w)))))
+(\lambda (c3: C).(\lambda (_: T).(\lambda (_: A).(csubc g e c3)))) (\lambda
+(_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g (asucc g a) e u)))) (\lambda
+(c3: C).(\lambda (w: T).(\lambda (a: A).(sc3 g a c3 w)))) (ex2 C (\lambda
+(e2: C).(clear c2 e2)) (\lambda (e2: C).(csubc g (CHead e (Bind b) u) e2)))
+(\lambda (x0: C).(\lambda (x1: T).(\lambda (x2: A).(\lambda (H3: (eq K (Bind
+b) (Bind Abst))).(\lambda (H4: (eq C c2 (CHead x0 (Bind Abbr) x1))).(\lambda
+(H5: (csubc g e x0)).(\lambda (H6: (sc3 g (asucc g x2) e u)).(\lambda (H7:
+(sc3 g x2 x0 x1)).(eq_ind_r C (CHead x0 (Bind Abbr) x1) (\lambda (c: C).(ex2
+C (\lambda (e2: C).(clear c e2)) (\lambda (e2: C).(csubc g (CHead e (Bind b)
+u) e2)))) (let H8 \def (f_equal K B (\lambda (e0: K).(match e0 in K return
+(\lambda (_: K).B) with [(Bind b0) \Rightarrow b0 | (Flat _) \Rightarrow b]))
+(Bind b) (Bind Abst) H3) in (eq_ind_r B Abst (\lambda (b0: B).(ex2 C (\lambda
+(e2: C).(clear (CHead x0 (Bind Abbr) x1) e2)) (\lambda (e2: C).(csubc g
+(CHead e (Bind b0) u) e2)))) (ex_intro2 C (\lambda (e2: C).(clear (CHead x0
+(Bind Abbr) x1) e2)) (\lambda (e2: C).(csubc g (CHead e (Bind Abst) u) e2))
+(CHead x0 (Bind Abbr) x1) (clear_bind Abbr x0 x1) (csubc_abst g e x0 H5 u x2
+H6 x1 H7)) b H8)) c2 H4))))))))) H2)) (\lambda (H2: (ex4_3 B C T (\lambda
+(b0: B).(\lambda (c3: C).(\lambda (v2: T).(eq C c2 (CHead c3 (Bind b0)
+v2))))) (\lambda (_: B).(\lambda (_: C).(\lambda (_: T).(eq K (Bind b) (Bind
+Void))))) (\lambda (b0: B).(\lambda (_: C).(\lambda (_: T).(not (eq B b0
+Void))))) (\lambda (_: B).(\lambda (c3: C).(\lambda (_: T).(csubc g e
+c3)))))).(ex4_3_ind B C T (\lambda (b0: B).(\lambda (c3: C).(\lambda (v2:
+T).(eq C c2 (CHead c3 (Bind b0) v2))))) (\lambda (_: B).(\lambda (_:
+C).(\lambda (_: T).(eq K (Bind b) (Bind Void))))) (\lambda (b0: B).(\lambda
+(_: C).(\lambda (_: T).(not (eq B b0 Void))))) (\lambda (_: B).(\lambda (c3:
+C).(\lambda (_: T).(csubc g e c3)))) (ex2 C (\lambda (e2: C).(clear c2 e2))
+(\lambda (e2: C).(csubc g (CHead e (Bind b) u) e2))) (\lambda (x0:
+B).(\lambda (x1: C).(\lambda (x2: T).(\lambda (H3: (eq C c2 (CHead x1 (Bind
+x0) x2))).(\lambda (H4: (eq K (Bind b) (Bind Void))).(\lambda (H5: (not (eq B
+x0 Void))).(\lambda (H6: (csubc g e x1)).(eq_ind_r C (CHead x1 (Bind x0) x2)
+(\lambda (c: C).(ex2 C (\lambda (e2: C).(clear c e2)) (\lambda (e2: C).(csubc
+g (CHead e (Bind b) u) e2)))) (let H7 \def (f_equal K B (\lambda (e0:
+K).(match e0 in K return (\lambda (_: K).B) with [(Bind b0) \Rightarrow b0 |
+(Flat _) \Rightarrow b])) (Bind b) (Bind Void) H4) in (eq_ind_r B Void
+(\lambda (b0: B).(ex2 C (\lambda (e2: C).(clear (CHead x1 (Bind x0) x2) e2))
+(\lambda (e2: C).(csubc g (CHead e (Bind b0) u) e2)))) (ex_intro2 C (\lambda
+(e2: C).(clear (CHead x1 (Bind x0) x2) e2)) (\lambda (e2: C).(csubc g (CHead
+e (Bind Void) u) e2)) (CHead x1 (Bind x0) x2) (clear_bind x0 x1 x2)
+(csubc_void g e x1 H6 x0 H5 u x2)) b H7)) c2 H3)))))))) H2)) H1))))))))