-c1 e1)) (\lambda (c1: C).(csubc g (CHead c k t0) c1)))) (let H9 \def (match
-H6 in csubc return (\lambda (c0: C).(\lambda (c1: C).(\lambda (_: (csubc ? c0
-c1)).((eq C c0 (CHead x0 k x1)) \to ((eq C c1 e1) \to (ex2 C (\lambda (c3:
-C).(drop h (S n) c3 e1)) (\lambda (c3: C).(csubc g (CHead c k (lift h (r k n)
-x1)) c3)))))))) with [(csubc_sort n0) \Rightarrow (\lambda (H9: (eq C (CSort
-n0) (CHead x0 k x1))).(\lambda (H10: (eq C (CSort n0) e1)).((let H11 \def
-(eq_ind C (CSort n0) (\lambda (e: C).(match e in C return (\lambda (_:
-C).Prop) with [(CSort _) \Rightarrow True | (CHead _ _ _) \Rightarrow
-False])) I (CHead x0 k x1) H9) in (False_ind ((eq C (CSort n0) e1) \to (ex2 C
-(\lambda (c1: C).(drop h (S n) c1 e1)) (\lambda (c1: C).(csubc g (CHead c k
-(lift h (r k n) x1)) c1)))) H11)) H10))) | (csubc_head c1 c0 H9 k0 v)
-\Rightarrow (\lambda (H10: (eq C (CHead c1 k0 v) (CHead x0 k x1))).(\lambda
-(H11: (eq C (CHead c0 k0 v) e1)).((let H12 \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 c1 k0 v) (CHead x0 k x1) H10) in
-((let H13 \def (f_equal C K (\lambda (e: C).(match e in C return (\lambda (_:
-C).K) with [(CSort _) \Rightarrow k0 | (CHead _ k1 _) \Rightarrow k1]))
-(CHead c1 k0 v) (CHead x0 k x1) H10) in ((let H14 \def (f_equal C C (\lambda
-(e: C).(match e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c1
-| (CHead c3 _ _) \Rightarrow c3])) (CHead c1 k0 v) (CHead x0 k x1) H10) in
-(eq_ind C x0 (\lambda (c3: C).((eq K k0 k) \to ((eq T v x1) \to ((eq C (CHead
-c0 k0 v) e1) \to ((csubc g c3 c0) \to (ex2 C (\lambda (c4: C).(drop h (S n)
-c4 e1)) (\lambda (c4: C).(csubc g (CHead c k (lift h (r k n) x1)) c4))))))))
-(\lambda (H15: (eq K k0 k)).(eq_ind K k (\lambda (k1: K).((eq T v x1) \to
-((eq C (CHead c0 k1 v) e1) \to ((csubc g x0 c0) \to (ex2 C (\lambda (c3:
-C).(drop h (S n) c3 e1)) (\lambda (c3: C).(csubc g (CHead c k (lift h (r k n)
-x1)) c3))))))) (\lambda (H16: (eq T v x1)).(eq_ind T x1 (\lambda (t0: T).((eq
-C (CHead c0 k t0) e1) \to ((csubc g x0 c0) \to (ex2 C (\lambda (c3: C).(drop
-h (S n) c3 e1)) (\lambda (c3: C).(csubc g (CHead c k (lift h (r k n) x1))
-c3)))))) (\lambda (H17: (eq C (CHead c0 k x1) e1)).(eq_ind C (CHead c0 k x1)
-(\lambda (c3: C).((csubc g x0 c0) \to (ex2 C (\lambda (c4: C).(drop h (S n)
-c4 c3)) (\lambda (c4: C).(csubc g (CHead c k (lift h (r k n) x1)) c4)))))
-(\lambda (H18: (csubc g x0 c0)).(let H_x \def (H x0 (r k n) h H5 c0 H18) in
-(let H19 \def H_x in (ex2_ind C (\lambda (c3: C).(drop h (r k n) c3 c0))
-(\lambda (c3: C).(csubc g c c3)) (ex2 C (\lambda (c3: C).(drop h (S n) c3
-(CHead c0 k x1))) (\lambda (c3: C).(csubc g (CHead c k (lift h (r k n) x1))
-c3))) (\lambda (x: C).(\lambda (H20: (drop h (r k n) x c0)).(\lambda (H21:
-(csubc g c x)).(ex_intro2 C (\lambda (c3: C).(drop h (S n) c3 (CHead c0 k
-x1))) (\lambda (c3: C).(csubc g (CHead c k (lift h (r k n) x1)) c3)) (CHead x
-k (lift h (r k n) x1)) (drop_skip k h n x c0 H20 x1) (csubc_head g c x H21 k
-(lift h (r k n) x1)))))) H19)))) e1 H17)) v (sym_eq T v x1 H16))) k0 (sym_eq
-K k0 k H15))) c1 (sym_eq C c1 x0 H14))) H13)) H12)) H11 H9))) | (csubc_abst
-c1 c0 H9 v a H10 w H11) \Rightarrow (\lambda (H12: (eq C (CHead c1 (Bind
-Abst) v) (CHead x0 k x1))).(\lambda (H13: (eq C (CHead c0 (Bind Abbr) w)
-e1)).((let H14 \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 c1 (Bind Abst) v) (CHead x0 k x1) H12) in ((let H15 \def
-(f_equal C K (\lambda (e: C).(match e in C return (\lambda (_: C).K) with
-[(CSort _) \Rightarrow (Bind Abst) | (CHead _ k0 _) \Rightarrow k0])) (CHead
-c1 (Bind Abst) v) (CHead x0 k x1) H12) in ((let H16 \def (f_equal C C
-(\lambda (e: C).(match e in C return (\lambda (_: C).C) with [(CSort _)
-\Rightarrow c1 | (CHead c3 _ _) \Rightarrow c3])) (CHead c1 (Bind Abst) v)
-(CHead x0 k x1) H12) in (eq_ind C x0 (\lambda (c3: C).((eq K (Bind Abst) k)
-\to ((eq T v x1) \to ((eq C (CHead c0 (Bind Abbr) w) e1) \to ((csubc g c3 c0)
-\to ((sc3 g (asucc g a) c3 v) \to ((sc3 g a c0 w) \to (ex2 C (\lambda (c4:
-C).(drop h (S n) c4 e1)) (\lambda (c4: C).(csubc g (CHead c k (lift h (r k n)
-x1)) c4)))))))))) (\lambda (H17: (eq K (Bind Abst) k)).(eq_ind K (Bind Abst)
-(\lambda (k0: K).((eq T v x1) \to ((eq C (CHead c0 (Bind Abbr) w) e1) \to
-((csubc g x0 c0) \to ((sc3 g (asucc g a) x0 v) \to ((sc3 g a c0 w) \to (ex2 C
-(\lambda (c3: C).(drop h (S n) c3 e1)) (\lambda (c3: C).(csubc g (CHead c k0
-(lift h (r k0 n) x1)) c3))))))))) (\lambda (H18: (eq T v x1)).(eq_ind T x1
-(\lambda (t0: T).((eq C (CHead c0 (Bind Abbr) w) e1) \to ((csubc g x0 c0) \to
-((sc3 g (asucc g a) x0 t0) \to ((sc3 g a c0 w) \to (ex2 C (\lambda (c3:
-C).(drop h (S n) c3 e1)) (\lambda (c3: C).(csubc g (CHead c (Bind Abst) (lift
-h (r (Bind Abst) n) x1)) c3)))))))) (\lambda (H19: (eq C (CHead c0 (Bind
-Abbr) w) e1)).(eq_ind C (CHead c0 (Bind Abbr) w) (\lambda (c3: C).((csubc g
-x0 c0) \to ((sc3 g (asucc g a) x0 x1) \to ((sc3 g a c0 w) \to (ex2 C (\lambda
-(c4: C).(drop h (S n) c4 c3)) (\lambda (c4: C).(csubc g (CHead c (Bind Abst)
-(lift h (r (Bind Abst) n) x1)) c4))))))) (\lambda (H20: (csubc g x0
-c0)).(\lambda (H21: (sc3 g (asucc g a) x0 x1)).(\lambda (H22: (sc3 g a c0
-w)).(let H23 \def (eq_ind_r K k (\lambda (k0: K).(\forall (h0: nat).((drop h0
-n (CHead c k0 (lift h (r k0 n) x1)) (CHead x0 k0 x1)) \to (\forall (e3:
-C).((csubc g (CHead x0 k0 x1) e3) \to (ex2 C (\lambda (c3: C).(drop h0 n c3
-e3)) (\lambda (c3: C).(csubc g (CHead c k0 (lift h (r k0 n) x1)) c3))))))))
-H8 (Bind Abst) H17) in (let H24 \def (eq_ind_r K k (\lambda (k0: K).(drop h
-(r k0 n) c x0)) H5 (Bind Abst) H17) in (let H_x \def (H x0 (r (Bind Abst) n)
-h H24 c0 H20) in (let H25 \def H_x in (ex2_ind C (\lambda (c3: C).(drop h (r
-(Bind Abst) n) c3 c0)) (\lambda (c3: C).(csubc g c c3)) (ex2 C (\lambda (c3:
-C).(drop h (S n) c3 (CHead c0 (Bind Abbr) w))) (\lambda (c3: C).(csubc g
-(CHead c (Bind Abst) (lift h (r (Bind Abst) n) x1)) c3))) (\lambda (x:
-C).(\lambda (H26: (drop h (r (Bind Abst) n) x c0)).(\lambda (H27: (csubc g c
-x)).(ex_intro2 C (\lambda (c3: C).(drop h (S n) c3 (CHead c0 (Bind Abbr) w)))
-(\lambda (c3: C).(csubc g (CHead c (Bind Abst) (lift h (r (Bind Abst) n) x1))
-c3)) (CHead x (Bind Abbr) (lift h n w)) (drop_skip_bind h n x c0 H26 Abbr w)
-(csubc_abst g c x H27 (lift h (r (Bind Abst) n) x1) a (sc3_lift g (asucc g a)
-x0 x1 H21 c h (r (Bind Abst) n) H24) (lift h n w) (sc3_lift g a c0 w H22 x h
-n H26)))))) H25)))))))) e1 H19)) v (sym_eq T v x1 H18))) k H17)) c1 (sym_eq C
-c1 x0 H16))) H15)) H14)) H13 H9 H10 H11)))]) in (H9 (refl_equal C (CHead x0 k
-x1)) (refl_equal C e1))) t H4))))))))) (drop_gen_skip_l c e2 t h n k
-H1)))))))) d))))))) c2)).
+c1 e1)) (\lambda (c1: C).(csubc g (CHead c k t0) c1)))) (let H_x \def
+(csubc_gen_head_l g x0 e1 x1 k H6) in (let H9 \def H_x in (or3_ind (ex2 C
+(\lambda (c3: C).(eq C e1 (CHead c3 k x1))) (\lambda (c3: C).(csubc g x0
+c3))) (ex5_3 C T A (\lambda (_: C).(\lambda (_: T).(\lambda (_: A).(eq K k
+(Bind Abst))))) (\lambda (c3: C).(\lambda (w: T).(\lambda (_: A).(eq C e1
+(CHead c3 (Bind Abbr) w))))) (\lambda (c3: C).(\lambda (_: T).(\lambda (_:
+A).(csubc g x0 c3)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g
+(asucc g a) x0 x1)))) (\lambda (c3: C).(\lambda (w: T).(\lambda (a: A).(sc3 g
+a c3 w))))) (ex4_3 B C T (\lambda (b: B).(\lambda (c3: C).(\lambda (v2:
+T).(eq C e1 (CHead c3 (Bind b) v2))))) (\lambda (_: B).(\lambda (_:
+C).(\lambda (_: T).(eq K k (Bind Void))))) (\lambda (b: B).(\lambda (_:
+C).(\lambda (_: T).(not (eq B b Void))))) (\lambda (_: B).(\lambda (c3:
+C).(\lambda (_: T).(csubc g x0 c3))))) (ex2 C (\lambda (c1: C).(drop h (S n)
+c1 e1)) (\lambda (c1: C).(csubc g (CHead c k (lift h (r k n) x1)) c1)))
+(\lambda (H10: (ex2 C (\lambda (c3: C).(eq C e1 (CHead c3 k x1))) (\lambda
+(c3: C).(csubc g x0 c3)))).(ex2_ind C (\lambda (c3: C).(eq C e1 (CHead c3 k
+x1))) (\lambda (c3: C).(csubc g x0 c3)) (ex2 C (\lambda (c1: C).(drop h (S n)
+c1 e1)) (\lambda (c1: C).(csubc g (CHead c k (lift h (r k n) x1)) c1)))
+(\lambda (x: C).(\lambda (H11: (eq C e1 (CHead x k x1))).(\lambda (H12:
+(csubc g x0 x)).(eq_ind_r C (CHead x k x1) (\lambda (c0: C).(ex2 C (\lambda
+(c1: C).(drop h (S n) c1 c0)) (\lambda (c1: C).(csubc g (CHead c k (lift h (r
+k n) x1)) c1)))) (let H_x0 \def (H x0 (r k n) h H5 x H12) in (let H13 \def
+H_x0 in (ex2_ind C (\lambda (c1: C).(drop h (r k n) c1 x)) (\lambda (c1:
+C).(csubc g c c1)) (ex2 C (\lambda (c1: C).(drop h (S n) c1 (CHead x k x1)))
+(\lambda (c1: C).(csubc g (CHead c k (lift h (r k n) x1)) c1))) (\lambda (x2:
+C).(\lambda (H14: (drop h (r k n) x2 x)).(\lambda (H15: (csubc g c
+x2)).(ex_intro2 C (\lambda (c1: C).(drop h (S n) c1 (CHead x k x1))) (\lambda
+(c1: C).(csubc g (CHead c k (lift h (r k n) x1)) c1)) (CHead x2 k (lift h (r
+k n) x1)) (drop_skip k h n x2 x H14 x1) (csubc_head g c x2 H15 k (lift h (r k
+n) x1)))))) H13))) e1 H11)))) H10)) (\lambda (H10: (ex5_3 C T A (\lambda (_:
+C).(\lambda (_: T).(\lambda (_: A).(eq K k (Bind Abst))))) (\lambda (c3:
+C).(\lambda (w: T).(\lambda (_: A).(eq C e1 (CHead c3 (Bind Abbr) w)))))
+(\lambda (c3: C).(\lambda (_: T).(\lambda (_: A).(csubc g x0 c3)))) (\lambda
+(_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g (asucc g a) x0 x1)))) (\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 k (Bind Abst)))))
+(\lambda (c3: C).(\lambda (w: T).(\lambda (_: A).(eq C e1 (CHead c3 (Bind
+Abbr) w))))) (\lambda (c3: C).(\lambda (_: T).(\lambda (_: A).(csubc g x0
+c3)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g (asucc g a) x0
+x1)))) (\lambda (c3: C).(\lambda (w: T).(\lambda (a: A).(sc3 g a c3 w))))
+(ex2 C (\lambda (c1: C).(drop h (S n) c1 e1)) (\lambda (c1: C).(csubc g
+(CHead c k (lift h (r k n) x1)) c1))) (\lambda (x2: C).(\lambda (x3:
+T).(\lambda (x4: A).(\lambda (H11: (eq K k (Bind Abst))).(\lambda (H12: (eq C
+e1 (CHead x2 (Bind Abbr) x3))).(\lambda (H13: (csubc g x0 x2)).(\lambda (H14:
+(sc3 g (asucc g x4) x0 x1)).(\lambda (H15: (sc3 g x4 x2 x3)).(eq_ind_r C
+(CHead x2 (Bind Abbr) x3) (\lambda (c0: C).(ex2 C (\lambda (c1: C).(drop h (S
+n) c1 c0)) (\lambda (c1: C).(csubc g (CHead c k (lift h (r k n) x1)) c1))))
+(let H16 \def (eq_ind K k (\lambda (k0: K).(\forall (h0: nat).((drop h0 n
+(CHead c k0 (lift h (r k0 n) x1)) (CHead x0 k0 x1)) \to (\forall (e3:
+C).((csubc g (CHead x0 k0 x1) e3) \to (ex2 C (\lambda (c1: C).(drop h0 n c1
+e3)) (\lambda (c1: C).(csubc g (CHead c k0 (lift h (r k0 n) x1)) c1))))))))
+H8 (Bind Abst) H11) in (let H17 \def (eq_ind K k (\lambda (k0: K).(drop h (r
+k0 n) c x0)) H5 (Bind Abst) H11) in (eq_ind_r K (Bind Abst) (\lambda (k0:
+K).(ex2 C (\lambda (c1: C).(drop h (S n) c1 (CHead x2 (Bind Abbr) x3)))
+(\lambda (c1: C).(csubc g (CHead c k0 (lift h (r k0 n) x1)) c1)))) (let H_x0
+\def (H x0 (r (Bind Abst) n) h H17 x2 H13) in (let H18 \def H_x0 in (ex2_ind
+C (\lambda (c1: C).(drop h n c1 x2)) (\lambda (c1: C).(csubc g c c1)) (ex2 C
+(\lambda (c1: C).(drop h (S n) c1 (CHead x2 (Bind Abbr) x3))) (\lambda (c1:
+C).(csubc g (CHead c (Bind Abst) (lift h (r (Bind Abst) n) x1)) c1)))
+(\lambda (x: C).(\lambda (H19: (drop h n x x2)).(\lambda (H20: (csubc g c
+x)).(ex_intro2 C (\lambda (c1: C).(drop h (S n) c1 (CHead x2 (Bind Abbr)
+x3))) (\lambda (c1: C).(csubc g (CHead c (Bind Abst) (lift h (r (Bind Abst)
+n) x1)) c1)) (CHead x (Bind Abbr) (lift h n x3)) (drop_skip_bind h n x x2 H19
+Abbr x3) (csubc_abst g c x H20 (lift h (r (Bind Abst) n) x1) x4 (sc3_lift g
+(asucc g x4) x0 x1 H14 c h (r (Bind Abst) n) H17) (lift h n x3) (sc3_lift g
+x4 x2 x3 H15 x h n H19)))))) H18))) k H11))) e1 H12))))))))) H10)) (\lambda
+(H10: (ex4_3 B C T (\lambda (b: B).(\lambda (c3: C).(\lambda (v2: T).(eq C e1
+(CHead c3 (Bind b) v2))))) (\lambda (_: B).(\lambda (_: C).(\lambda (_:
+T).(eq K k (Bind Void))))) (\lambda (b: B).(\lambda (_: C).(\lambda (_:
+T).(not (eq B b Void))))) (\lambda (_: B).(\lambda (c3: C).(\lambda (_:
+T).(csubc g x0 c3)))))).(ex4_3_ind B C T (\lambda (b: B).(\lambda (c3:
+C).(\lambda (v2: T).(eq C e1 (CHead c3 (Bind b) v2))))) (\lambda (_:
+B).(\lambda (_: C).(\lambda (_: T).(eq K k (Bind Void))))) (\lambda (b:
+B).(\lambda (_: C).(\lambda (_: T).(not (eq B b Void))))) (\lambda (_:
+B).(\lambda (c3: C).(\lambda (_: T).(csubc g x0 c3)))) (ex2 C (\lambda (c1:
+C).(drop h (S n) c1 e1)) (\lambda (c1: C).(csubc g (CHead c k (lift h (r k n)
+x1)) c1))) (\lambda (x2: B).(\lambda (x3: C).(\lambda (x4: T).(\lambda (H11:
+(eq C e1 (CHead x3 (Bind x2) x4))).(\lambda (H12: (eq K k (Bind
+Void))).(\lambda (H13: (not (eq B x2 Void))).(\lambda (H14: (csubc g x0
+x3)).(eq_ind_r C (CHead x3 (Bind x2) x4) (\lambda (c0: C).(ex2 C (\lambda
+(c1: C).(drop h (S n) c1 c0)) (\lambda (c1: C).(csubc g (CHead c k (lift h (r
+k n) x1)) c1)))) (let H15 \def (eq_ind K k (\lambda (k0: K).(\forall (h0:
+nat).((drop h0 n (CHead c k0 (lift h (r k0 n) x1)) (CHead x0 k0 x1)) \to
+(\forall (e3: C).((csubc g (CHead x0 k0 x1) e3) \to (ex2 C (\lambda (c1:
+C).(drop h0 n c1 e3)) (\lambda (c1: C).(csubc g (CHead c k0 (lift h (r k0 n)
+x1)) c1)))))))) H8 (Bind Void) H12) in (let H16 \def (eq_ind K k (\lambda
+(k0: K).(drop h (r k0 n) c x0)) H5 (Bind Void) H12) in (eq_ind_r K (Bind
+Void) (\lambda (k0: K).(ex2 C (\lambda (c1: C).(drop h (S n) c1 (CHead x3
+(Bind x2) x4))) (\lambda (c1: C).(csubc g (CHead c k0 (lift h (r k0 n) x1))
+c1)))) (let H_x0 \def (H x0 (r (Bind Void) n) h H16 x3 H14) in (let H17 \def
+H_x0 in (ex2_ind C (\lambda (c1: C).(drop h n c1 x3)) (\lambda (c1: C).(csubc
+g c c1)) (ex2 C (\lambda (c1: C).(drop h (S n) c1 (CHead x3 (Bind x2) x4)))
+(\lambda (c1: C).(csubc g (CHead c (Bind Void) (lift h (r (Bind Void) n) x1))
+c1))) (\lambda (x: C).(\lambda (H18: (drop h n x x3)).(\lambda (H19: (csubc g
+c x)).(ex_intro2 C (\lambda (c1: C).(drop h (S n) c1 (CHead x3 (Bind x2)
+x4))) (\lambda (c1: C).(csubc g (CHead c (Bind Void) (lift h (r (Bind Void)
+n) x1)) c1)) (CHead x (Bind x2) (lift h n x4)) (drop_skip_bind h n x x3 H18
+x2 x4) (csubc_void g c x H19 x2 H13 (lift h (r (Bind Void) n) x1) (lift h n
+x4)))))) H17))) k H12))) e1 H11)))))))) H10)) H9))) t H4)))))))))
+(drop_gen_skip_l c e2 t h n k H1)))))))) d))))))) c2)).