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