-d2)))))) (\lambda (H5: (csuba g (CHead c (Bind Abbr) t) c2)).(\lambda (H6:
-(drop (r (Bind Abbr) n) O c (CHead d1 (Bind Abbr) u))).(let H_x \def
-(csuba_gen_abbr g c c2 t H5) in (let H7 \def H_x in (ex2_ind C (\lambda (d2:
-C).(eq C c2 (CHead d2 (Bind Abbr) t))) (\lambda (d2: C).(csuba g c d2)) (ex2
-C (\lambda (d2: C).(drop (S n) O c2 (CHead d2 (Bind Abbr) u))) (\lambda (d2:
-C).(csuba g d1 d2))) (\lambda (x: C).(\lambda (H8: (eq C c2 (CHead x (Bind
-Abbr) t))).(\lambda (H9: (csuba g c x)).(eq_ind_r C (CHead x (Bind Abbr) t)
-(\lambda (c0: C).(ex2 C (\lambda (d2: C).(drop (S n) O c0 (CHead d2 (Bind
-Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)))) (let H10 \def (H c d1 u H6 g x
-H9) in (ex2_ind C (\lambda (d2: C).(drop n O x (CHead d2 (Bind Abbr) u)))
-(\lambda (d2: C).(csuba g d1 d2)) (ex2 C (\lambda (d2: C).(drop (S n) O
-(CHead x (Bind Abbr) t) (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g
-d1 d2))) (\lambda (x0: C).(\lambda (H11: (drop n O x (CHead x0 (Bind Abbr)
-u))).(\lambda (H12: (csuba g d1 x0)).(let H13 \def (refl_equal nat (r (Bind
-Abbr) n)) in (let H14 \def (eq_ind nat n (\lambda (n0: nat).(drop n0 O x
-(CHead x0 (Bind Abbr) u))) H11 (r (Bind Abbr) n) H13) in (ex_intro2 C
-(\lambda (d2: C).(drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Abbr)
-u))) (\lambda (d2: C).(csuba g d1 d2)) x0 (drop_drop (Bind Abbr) n x (CHead
-x0 (Bind Abbr) u) H14 t) H12)))))) H10)) c2 H8)))) H7))))) (\lambda (H5:
-(csuba g (CHead c (Bind Abst) t) c2)).(\lambda (H6: (drop (r (Bind Abst) n) O
-c (CHead d1 (Bind Abbr) u))).(let H_x \def (csuba_gen_abst g c c2 t H5) in
-(let H7 \def H_x in (or_ind (ex2 C (\lambda (d2: C).(eq C c2 (CHead d2 (Bind
-Abst) t))) (\lambda (d2: C).(csuba g c d2))) (ex4_3 C T A (\lambda (d2:
-C).(\lambda (u2: T).(\lambda (_: A).(eq C c2 (CHead d2 (Bind Abbr) u2)))))
-(\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g c d2)))) (\lambda
-(_: C).(\lambda (_: T).(\lambda (a: A).(arity g c t (asucc g a))))) (\lambda
-(d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a))))) (ex2 C
-(\lambda (d2: C).(drop (S n) O c2 (CHead d2 (Bind Abbr) u))) (\lambda (d2:
-C).(csuba g d1 d2))) (\lambda (H8: (ex2 C (\lambda (d2: C).(eq C c2 (CHead d2
-(Bind Abst) t))) (\lambda (d2: C).(csuba g c d2)))).(ex2_ind C (\lambda (d2:
-C).(eq C c2 (CHead d2 (Bind Abst) t))) (\lambda (d2: C).(csuba g c d2)) (ex2
-C (\lambda (d2: C).(drop (S n) O c2 (CHead d2 (Bind Abbr) u))) (\lambda (d2:
-C).(csuba g d1 d2))) (\lambda (x: C).(\lambda (H9: (eq C c2 (CHead x (Bind
-Abst) t))).(\lambda (H10: (csuba g c x)).(eq_ind_r C (CHead x (Bind Abst) t)
-(\lambda (c0: C).(ex2 C (\lambda (d2: C).(drop (S n) O c0 (CHead d2 (Bind
-Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)))) (let H11 \def (H c d1 u H6 g x
-H10) in (ex2_ind C (\lambda (d2: C).(drop n O x (CHead d2 (Bind Abbr) u)))
-(\lambda (d2: C).(csuba g d1 d2)) (ex2 C (\lambda (d2: C).(drop (S n) O
-(CHead x (Bind Abst) t) (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g
-d1 d2))) (\lambda (x0: C).(\lambda (H12: (drop n O x (CHead x0 (Bind Abbr)
-u))).(\lambda (H13: (csuba g d1 x0)).(let H14 \def (refl_equal nat (r (Bind
-Abbr) n)) in (let H15 \def (eq_ind nat n (\lambda (n0: nat).(drop n0 O x
-(CHead x0 (Bind Abbr) u))) H12 (r (Bind Abbr) n) H14) in (ex_intro2 C
-(\lambda (d2: C).(drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Abbr)
-u))) (\lambda (d2: C).(csuba g d1 d2)) x0 (drop_drop (Bind Abst) n x (CHead
-x0 (Bind Abbr) u) H15 t) H13)))))) H11)) c2 H9)))) H8)) (\lambda (H8: (ex4_3
-C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c2 (CHead d2
-(Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g
-c d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g c t (asucc
-g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
-a)))))).(ex4_3_ind C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_:
-A).(eq C c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_:
+d2))))))))))).(\lambda (k: K).(\lambda (t: T).(\lambda (d1: C).(\lambda (u:
+T).(\lambda (H1: (drop (S n) O (CHead c k t) (CHead d1 (Bind Abbr)
+u))).(\lambda (g: G).(\lambda (c2: C).(\lambda (H2: (csuba g (CHead c k t)
+c2)).(K_ind (\lambda (k0: K).((csuba g (CHead c k0 t) c2) \to ((drop (r k0 n)
+O c (CHead d1 (Bind Abbr) u)) \to (ex2 C (\lambda (d2: C).(drop (S n) O c2
+(CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)))))) (\lambda (b:
+B).(\lambda (H3: (csuba g (CHead c (Bind b) t) c2)).(\lambda (H4: (drop (r
+(Bind b) n) O c (CHead d1 (Bind Abbr) u))).(B_ind (\lambda (b0: B).((csuba g
+(CHead c (Bind b0) t) c2) \to ((drop (r (Bind b0) n) O c (CHead d1 (Bind
+Abbr) u)) \to (ex2 C (\lambda (d2: C).(drop (S n) O c2 (CHead d2 (Bind Abbr)
+u))) (\lambda (d2: C).(csuba g d1 d2)))))) (\lambda (H5: (csuba g (CHead c
+(Bind Abbr) t) c2)).(\lambda (H6: (drop (r (Bind Abbr) n) O c (CHead d1 (Bind
+Abbr) u))).(let H_x \def (csuba_gen_abbr g c c2 t H5) in (let H7 \def H_x in
+(ex2_ind C (\lambda (d2: C).(eq C c2 (CHead d2 (Bind Abbr) t))) (\lambda (d2:
+C).(csuba g c d2)) (ex2 C (\lambda (d2: C).(drop (S n) O c2 (CHead d2 (Bind
+Abbr) u))) (\lambda (d2: C).(csuba g d1 d2))) (\lambda (x: C).(\lambda (H8:
+(eq C c2 (CHead x (Bind Abbr) t))).(\lambda (H9: (csuba g c x)).(eq_ind_r C
+(CHead x (Bind Abbr) t) (\lambda (c0: C).(ex2 C (\lambda (d2: C).(drop (S n)
+O c0 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)))) (let H10
+\def (H c d1 u H6 g x H9) in (ex2_ind C (\lambda (d2: C).(drop n O x (CHead
+d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)) (ex2 C (\lambda (d2:
+C).(drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Abbr) u))) (\lambda
+(d2: C).(csuba g d1 d2))) (\lambda (x0: C).(\lambda (H11: (drop n O x (CHead
+x0 (Bind Abbr) u))).(\lambda (H12: (csuba g d1 x0)).(let H13 \def (refl_equal
+nat (r (Bind Abbr) n)) in (let H14 \def (eq_ind nat n (\lambda (n0:
+nat).(drop n0 O x (CHead x0 (Bind Abbr) u))) H11 (r (Bind Abbr) n) H13) in
+(ex_intro2 C (\lambda (d2: C).(drop (S n) O (CHead x (Bind Abbr) t) (CHead d2
+(Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)) x0 (drop_drop (Bind Abbr)
+n x (CHead x0 (Bind Abbr) u) H14 t) H12)))))) H10)) c2 H8)))) H7)))))
+(\lambda (H5: (csuba g (CHead c (Bind Abst) t) c2)).(\lambda (H6: (drop (r
+(Bind Abst) n) O c (CHead d1 (Bind Abbr) u))).(let H_x \def (csuba_gen_abst g
+c c2 t H5) in (let H7 \def H_x in (or_ind (ex2 C (\lambda (d2: C).(eq C c2
+(CHead d2 (Bind Abst) t))) (\lambda (d2: C).(csuba g c d2))) (ex4_3 C T A
+(\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c2 (CHead d2 (Bind
+Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g c
+d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g c t (asucc g
+a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
+a))))) (ex2 C (\lambda (d2: C).(drop (S n) O c2 (CHead d2 (Bind Abbr) u)))
+(\lambda (d2: C).(csuba g d1 d2))) (\lambda (H8: (ex2 C (\lambda (d2: C).(eq
+C c2 (CHead d2 (Bind Abst) t))) (\lambda (d2: C).(csuba g c d2)))).(ex2_ind C
+(\lambda (d2: C).(eq C c2 (CHead d2 (Bind Abst) t))) (\lambda (d2: C).(csuba
+g c d2)) (ex2 C (\lambda (d2: C).(drop (S n) O c2 (CHead d2 (Bind Abbr) u)))
+(\lambda (d2: C).(csuba g d1 d2))) (\lambda (x: C).(\lambda (H9: (eq C c2
+(CHead x (Bind Abst) t))).(\lambda (H10: (csuba g c x)).(eq_ind_r C (CHead x
+(Bind Abst) t) (\lambda (c0: C).(ex2 C (\lambda (d2: C).(drop (S n) O c0
+(CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)))) (let H11 \def
+(H c d1 u H6 g x H10) in (ex2_ind C (\lambda (d2: C).(drop n O x (CHead d2
+(Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)) (ex2 C (\lambda (d2:
+C).(drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Abbr) u))) (\lambda
+(d2: C).(csuba g d1 d2))) (\lambda (x0: C).(\lambda (H12: (drop n O x (CHead
+x0 (Bind Abbr) u))).(\lambda (H13: (csuba g d1 x0)).(let H14 \def (refl_equal
+nat (r (Bind Abbr) n)) in (let H15 \def (eq_ind nat n (\lambda (n0:
+nat).(drop n0 O x (CHead x0 (Bind Abbr) u))) H12 (r (Bind Abbr) n) H14) in
+(ex_intro2 C (\lambda (d2: C).(drop (S n) O (CHead x (Bind Abst) t) (CHead d2
+(Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)) x0 (drop_drop (Bind Abst)
+n x (CHead x0 (Bind Abbr) u) H15 t) H13)))))) H11)) c2 H9)))) H8)) (\lambda
+(H8: (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c2
+(CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
+A).(csuba g c d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g
+c t (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity
+g d2 u2 a)))))).(ex4_3_ind C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda
+(_: A).(eq C c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: