-C).(match e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow d1 |
-(CHead c _ _) \Rightarrow c])) (CHead d1 (Bind Abst) t) (CHead x0 (Bind b)
-t0) (clear_gen_bind b x0 (CHead d1 (Bind Abst) t) t0 H6)) in ((let H8 \def
-(f_equal C B (\lambda (e: C).(match e in C return (\lambda (_: C).B) with
-[(CSort _) \Rightarrow Abst | (CHead _ k0 _) \Rightarrow (match k0 in K
-return (\lambda (_: K).B) with [(Bind b0) \Rightarrow b0 | (Flat _)
-\Rightarrow Abst])])) (CHead d1 (Bind Abst) t) (CHead x0 (Bind b) t0)
-(clear_gen_bind b x0 (CHead d1 (Bind Abst) t) t0 H6)) in ((let H9 \def
-(f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with
-[(CSort _) \Rightarrow t | (CHead _ _ t1) \Rightarrow t1])) (CHead d1 (Bind
-Abst) t) (CHead x0 (Bind b) t0) (clear_gen_bind b x0 (CHead d1 (Bind Abst) t)
-t0 H6)) in (\lambda (H10: (eq B Abst b)).(\lambda (H11: (eq C d1
-x0)).(\lambda (c2: C).(\lambda (H12: (csubt g c1 c2)).(let H13 \def (eq_ind_r
-T t0 (\lambda (t1: T).(drop n O c1 (CHead x0 (Bind b) t1))) H5 t H9) in (let
-H14 \def (eq_ind_r B b (\lambda (b0: B).(drop n O c1 (CHead x0 (Bind b0) t)))
-H13 Abst H10) in (let H15 \def (eq_ind_r C x0 (\lambda (c: C).(drop n O c1
-(CHead c (Bind Abst) t))) H14 d1 H11) in (or_ind (ex2 C (\lambda (d2:
-C).(csubt g d1 d2)) (\lambda (d2: C).(drop n O c2 (CHead d2 (Bind Abst) t))))
-(ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2:
-C).(\lambda (u: T).(drop n O c2 (CHead d2 (Bind Abbr) u)))) (\lambda (_:
-C).(\lambda (u: T).(ty3 g d1 u t))) (\lambda (d2: C).(\lambda (u: T).(ty3 g
-d2 u t)))) (or (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
-C).(getl n c2 (CHead d2 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2:
-C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(getl n
-c2 (CHead d2 (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u
-t))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t))))) (\lambda (H16: (ex2
-C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop n O c2 (CHead d2
-(Bind Abst) t))))).(ex2_ind C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
-C).(drop n O c2 (CHead d2 (Bind Abst) t))) (or (ex2 C (\lambda (d2: C).(csubt
-g d1 d2)) (\lambda (d2: C).(getl n c2 (CHead d2 (Bind Abst) t)))) (ex4_2 C T
-(\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda
-(u: T).(getl n c2 (CHead d2 (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u:
-T).(ty3 g d1 u t))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t)))))
-(\lambda (x1: C).(\lambda (H17: (csubt g d1 x1)).(\lambda (H18: (drop n O c2
-(CHead x1 (Bind Abst) t))).(or_introl (ex2 C (\lambda (d2: C).(csubt g d1
+C).(match e with [(CSort _) \Rightarrow d1 | (CHead c _ _) \Rightarrow c]))
+(CHead d1 (Bind Abst) t) (CHead x0 (Bind b) t0) (clear_gen_bind b x0 (CHead
+d1 (Bind Abst) t) t0 H6)) in ((let H8 \def (f_equal C B (\lambda (e:
+C).(match e with [(CSort _) \Rightarrow Abst | (CHead _ k0 _) \Rightarrow
+(match k0 with [(Bind b0) \Rightarrow b0 | (Flat _) \Rightarrow Abst])]))
+(CHead d1 (Bind Abst) t) (CHead x0 (Bind b) t0) (clear_gen_bind b x0 (CHead
+d1 (Bind Abst) t) t0 H6)) in ((let H9 \def (f_equal C T (\lambda (e:
+C).(match e with [(CSort _) \Rightarrow t | (CHead _ _ t1) \Rightarrow t1]))
+(CHead d1 (Bind Abst) t) (CHead x0 (Bind b) t0) (clear_gen_bind b x0 (CHead
+d1 (Bind Abst) t) t0 H6)) in (\lambda (H10: (eq B Abst b)).(\lambda (H11: (eq
+C d1 x0)).(\lambda (c2: C).(\lambda (H12: (csubt g c1 c2)).(let H13 \def
+(eq_ind_r T t0 (\lambda (t1: T).(drop n O c1 (CHead x0 (Bind b) t1))) H5 t
+H9) in (let H14 \def (eq_ind_r B b (\lambda (b0: B).(drop n O c1 (CHead x0
+(Bind b0) t))) H13 Abst H10) in (let H15 \def (eq_ind_r C x0 (\lambda (c:
+C).(drop n O c1 (CHead c (Bind Abst) t))) H14 d1 H11) in (or_ind (ex2 C
+(\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop n O c2 (CHead d2
+(Bind Abst) t)))) (ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1
+d2))) (\lambda (d2: C).(\lambda (u: T).(drop n O c2 (CHead d2 (Bind Abbr)
+u)))) (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u t))) (\lambda (d2:
+C).(\lambda (u: T).(ty3 g d2 u t)))) (or (ex2 C (\lambda (d2: C).(csubt g d1