-H15 g c2 H12) in (ex2_ind C (\lambda (d2: C).(drop i O c2 (CHead d2 (Bind
-Abst) u))) (\lambda (d2: C).(csuba g d2 d1)) (ex2 C (\lambda (d2: C).(getl i
-c2 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1))) (\lambda
-(x1: C).(\lambda (H17: (drop i O c2 (CHead x1 (Bind Abst) u))).(\lambda (H18:
-(csuba g x1 d1)).(ex_intro2 C (\lambda (d2: C).(getl i c2 (CHead d2 (Bind
-Abst) u))) (\lambda (d2: C).(csuba g d2 d1)) x1 (getl_intro i c2 (CHead x1
-(Bind Abst) u) (CHead x1 (Bind Abst) u) H17 (clear_bind Abst x1 u)) H18))))
-H16)))))))))) H8)) H7))))) (\lambda (f: F).(\lambda (H5: (drop i O c1 (CHead
-x0 (Flat f) t))).(\lambda (H6: (clear (CHead x0 (Flat f) t) (CHead d1 (Bind
-Abst) u))).(let H7 \def H5 in (unintro C c1 (\lambda (c: C).((drop i O c
-(CHead x0 (Flat f) t)) \to (\forall (c2: C).((csuba g c2 c) \to (ex2 C
-(\lambda (d2: C).(getl i c2 (CHead d2 (Bind Abst) u))) (\lambda (d2:
-C).(csuba g d2 d1))))))) (nat_ind (\lambda (n: nat).(\forall (x1: C).((drop n
-O x1 (CHead x0 (Flat f) t)) \to (\forall (c2: C).((csuba g c2 x1) \to (ex2 C
-(\lambda (d2: C).(getl n c2 (CHead d2 (Bind Abst) u))) (\lambda (d2:
-C).(csuba g d2 d1)))))))) (\lambda (x1: C).(\lambda (H8: (drop O O x1 (CHead
-x0 (Flat f) t))).(\lambda (c2: C).(\lambda (H9: (csuba g c2 x1)).(let H10
-\def (eq_ind C x1 (\lambda (c: C).(csuba g c2 c)) H9 (CHead x0 (Flat f) t)
-(drop_gen_refl x1 (CHead x0 (Flat f) t) H8)) in (let H_y \def (clear_flat x0
-(CHead d1 (Bind Abst) u) (clear_gen_flat f x0 (CHead d1 (Bind Abst) u) t H6)
-f t) in (let H11 \def (csuba_clear_trans g (CHead x0 (Flat f) t) c2 H10
-(CHead d1 (Bind Abst) u) H_y) in (ex2_ind C (\lambda (e2: C).(csuba g e2
-(CHead d1 (Bind Abst) u))) (\lambda (e2: C).(clear c2 e2)) (ex2 C (\lambda
-(d2: C).(getl O c2 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2
-d1))) (\lambda (x2: C).(\lambda (H12: (csuba g x2 (CHead d1 (Bind Abst)
-u))).(\lambda (H13: (clear c2 x2)).(let H_x \def (csuba_gen_abst_rev g d1 x2
-u H12) in (let H14 \def H_x in (ex2_ind C (\lambda (d2: C).(eq C x2 (CHead d2
-(Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1)) (ex2 C (\lambda (d2:
-C).(getl O c2 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1)))
-(\lambda (x3: C).(\lambda (H15: (eq C x2 (CHead x3 (Bind Abst) u))).(\lambda
-(H16: (csuba g x3 d1)).(let H17 \def (eq_ind C x2 (\lambda (c: C).(clear c2
-c)) H13 (CHead x3 (Bind Abst) u) H15) in (ex_intro2 C (\lambda (d2: C).(getl
-O c2 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1)) x3
-(getl_intro O c2 (CHead x3 (Bind Abst) u) c2 (drop_refl c2) H17) H16)))))
-H14)))))) H11)))))))) (\lambda (n: nat).(\lambda (H8: ((\forall (x1:
-C).((drop n O x1 (CHead x0 (Flat f) t)) \to (\forall (c2: C).((csuba g c2 x1)
-\to (ex2 C (\lambda (d2: C).(getl n c2 (CHead d2 (Bind Abst) u))) (\lambda
-(d2: C).(csuba g d2 d1))))))))).(\lambda (x1: C).(\lambda (H9: (drop (S n) O
-x1 (CHead x0 (Flat f) t))).(\lambda (c2: C).(\lambda (H10: (csuba g c2
-x1)).(let H11 \def (drop_clear x1 (CHead x0 (Flat f) t) n H9) in (ex2_3_ind B
-C T (\lambda (b: B).(\lambda (e: C).(\lambda (v: T).(clear x1 (CHead e (Bind
-b) v))))) (\lambda (_: B).(\lambda (e: C).(\lambda (_: T).(drop n O e (CHead
-x0 (Flat f) t))))) (ex2 C (\lambda (d2: C).(getl (S n) c2 (CHead d2 (Bind
-Abst) u))) (\lambda (d2: C).(csuba g d2 d1))) (\lambda (x2: B).(\lambda (x3:
-C).(\lambda (x4: T).(\lambda (H12: (clear x1 (CHead x3 (Bind x2)
-x4))).(\lambda (H13: (drop n O x3 (CHead x0 (Flat f) t))).(let H14 \def
+H15 g c2 H12) in (or_ind (ex2 C (\lambda (d2: C).(drop i O c2 (CHead d2 (Bind
+Abst) u))) (\lambda (d2: C).(csuba g d2 d1))) (ex2_2 C T (\lambda (d2:
+C).(\lambda (u2: T).(drop i O c2 (CHead d2 (Bind Void) u2)))) (\lambda (d2:
+C).(\lambda (_: T).(csuba g d2 d1)))) (or (ex2 C (\lambda (d2: C).(getl i c2
+(CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1))) (ex2_2 C T
+(\lambda (d2: C).(\lambda (u2: T).(getl i c2 (CHead d2 (Bind Void) u2))))
+(\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))) (\lambda (H17: (ex2 C
+(\lambda (d2: C).(drop i O c2 (CHead d2 (Bind Abst) u))) (\lambda (d2:
+C).(csuba g d2 d1)))).(ex2_ind C (\lambda (d2: C).(drop i O c2 (CHead d2
+(Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1)) (or (ex2 C (\lambda (d2:
+C).(getl i c2 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1)))
+(ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(getl i c2 (CHead d2 (Bind Void)
+u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))) (\lambda (x1:
+C).(\lambda (H18: (drop i O c2 (CHead x1 (Bind Abst) u))).(\lambda (H19:
+(csuba g x1 d1)).(or_introl (ex2 C (\lambda (d2: C).(getl i c2 (CHead d2
+(Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1))) (ex2_2 C T (\lambda (d2:
+C).(\lambda (u2: T).(getl i c2 (CHead d2 (Bind Void) u2)))) (\lambda (d2:
+C).(\lambda (_: T).(csuba g d2 d1)))) (ex_intro2 C (\lambda (d2: C).(getl i
+c2 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1)) x1
+(getl_intro i c2 (CHead x1 (Bind Abst) u) (CHead x1 (Bind Abst) u) H18
+(clear_bind Abst x1 u)) H19))))) H17)) (\lambda (H17: (ex2_2 C T (\lambda
+(d2: C).(\lambda (u2: T).(drop i O c2 (CHead d2 (Bind Void) u2)))) (\lambda
+(d2: C).(\lambda (_: T).(csuba g d2 d1))))).(ex2_2_ind C T (\lambda (d2:
+C).(\lambda (u2: T).(drop i O c2 (CHead d2 (Bind Void) u2)))) (\lambda (d2:
+C).(\lambda (_: T).(csuba g d2 d1))) (or (ex2 C (\lambda (d2: C).(getl i c2
+(CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1))) (ex2_2 C T
+(\lambda (d2: C).(\lambda (u2: T).(getl i c2 (CHead d2 (Bind Void) u2))))
+(\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))) (\lambda (x1:
+C).(\lambda (x2: T).(\lambda (H18: (drop i O c2 (CHead x1 (Bind Void)
+x2))).(\lambda (H19: (csuba g x1 d1)).(or_intror (ex2 C (\lambda (d2:
+C).(getl i c2 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1)))
+(ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(getl i c2 (CHead d2 (Bind Void)
+u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1)))) (ex2_2_intro C T
+(\lambda (d2: C).(\lambda (u2: T).(getl i c2 (CHead d2 (Bind Void) u2))))
+(\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))) x1 x2 (getl_intro i c2
+(CHead x1 (Bind Void) x2) (CHead x1 (Bind Void) x2) H18 (clear_bind Void x1
+x2)) H19)))))) H17)) H16)))))))))) H8)) H7))))) (\lambda (f: F).(\lambda (H5:
+(drop i O c1 (CHead x0 (Flat f) t))).(\lambda (H6: (clear (CHead x0 (Flat f)
+t) (CHead d1 (Bind Abst) u))).(let H7 \def H5 in (unintro C c1 (\lambda (c:
+C).((drop i O c (CHead x0 (Flat f) t)) \to (\forall (c2: C).((csuba g c2 c)
+\to (or (ex2 C (\lambda (d2: C).(getl i c2 (CHead d2 (Bind Abst) u)))
+(\lambda (d2: C).(csuba g d2 d1))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2:
+T).(getl i c2 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_:
+T).(csuba g d2 d1))))))))) (nat_ind (\lambda (n: nat).(\forall (x1: C).((drop
+n O x1 (CHead x0 (Flat f) t)) \to (\forall (c2: C).((csuba g c2 x1) \to (or
+(ex2 C (\lambda (d2: C).(getl n c2 (CHead d2 (Bind Abst) u))) (\lambda (d2:
+C).(csuba g d2 d1))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(getl n c2
+(CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2
+d1)))))))))) (\lambda (x1: C).(\lambda (H8: (drop O O x1 (CHead x0 (Flat f)
+t))).(\lambda (c2: C).(\lambda (H9: (csuba g c2 x1)).(let H10 \def (eq_ind C
+x1 (\lambda (c: C).(csuba g c2 c)) H9 (CHead x0 (Flat f) t) (drop_gen_refl x1
+(CHead x0 (Flat f) t) H8)) in (let H_y \def (clear_flat x0 (CHead d1 (Bind
+Abst) u) (clear_gen_flat f x0 (CHead d1 (Bind Abst) u) t H6) f t) in (let H11
+\def (csuba_clear_trans g (CHead x0 (Flat f) t) c2 H10 (CHead d1 (Bind Abst)
+u) H_y) in (ex2_ind C (\lambda (e2: C).(csuba g e2 (CHead d1 (Bind Abst) u)))
+(\lambda (e2: C).(clear c2 e2)) (or (ex2 C (\lambda (d2: C).(getl O c2 (CHead
+d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1))) (ex2_2 C T (\lambda
+(d2: C).(\lambda (u2: T).(getl O c2 (CHead d2 (Bind Void) u2)))) (\lambda
+(d2: C).(\lambda (_: T).(csuba g d2 d1))))) (\lambda (x2: C).(\lambda (H12:
+(csuba g x2 (CHead d1 (Bind Abst) u))).(\lambda (H13: (clear c2 x2)).(let H_x
+\def (csuba_gen_abst_rev g d1 x2 u H12) in (let H14 \def H_x in (or_ind (ex2
+C (\lambda (d2: C).(eq C x2 (CHead d2 (Bind Abst) u))) (\lambda (d2:
+C).(csuba g d2 d1))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq C x2
+(CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2
+d1)))) (or (ex2 C (\lambda (d2: C).(getl O c2 (CHead d2 (Bind Abst) u)))
+(\lambda (d2: C).(csuba g d2 d1))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2:
+T).(getl O c2 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_:
+T).(csuba g d2 d1))))) (\lambda (H15: (ex2 C (\lambda (d2: C).(eq C x2 (CHead
+d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1)))).(ex2_ind C (\lambda
+(d2: C).(eq C x2 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1))
+(or (ex2 C (\lambda (d2: C).(getl O c2 (CHead d2 (Bind Abst) u))) (\lambda
+(d2: C).(csuba g d2 d1))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(getl
+O c2 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g
+d2 d1))))) (\lambda (x3: C).(\lambda (H16: (eq C x2 (CHead x3 (Bind Abst)
+u))).(\lambda (H17: (csuba g x3 d1)).(let H18 \def (eq_ind C x2 (\lambda (c:
+C).(clear c2 c)) H13 (CHead x3 (Bind Abst) u) H16) in (or_introl (ex2 C
+(\lambda (d2: C).(getl O c2 (CHead d2 (Bind Abst) u))) (\lambda (d2:
+C).(csuba g d2 d1))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(getl O c2
+(CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2
+d1)))) (ex_intro2 C (\lambda (d2: C).(getl O c2 (CHead d2 (Bind Abst) u)))
+(\lambda (d2: C).(csuba g d2 d1)) x3 (getl_intro O c2 (CHead x3 (Bind Abst)
+u) c2 (drop_refl c2) H18) H17)))))) H15)) (\lambda (H15: (ex2_2 C T (\lambda
+(d2: C).(\lambda (u2: T).(eq C x2 (CHead d2 (Bind Void) u2)))) (\lambda (d2:
+C).(\lambda (_: T).(csuba g d2 d1))))).(ex2_2_ind C T (\lambda (d2:
+C).(\lambda (u2: T).(eq C x2 (CHead d2 (Bind Void) u2)))) (\lambda (d2:
+C).(\lambda (_: T).(csuba g d2 d1))) (or (ex2 C (\lambda (d2: C).(getl O c2
+(CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1))) (ex2_2 C T
+(\lambda (d2: C).(\lambda (u2: T).(getl O c2 (CHead d2 (Bind Void) u2))))
+(\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))) (\lambda (x3:
+C).(\lambda (x4: T).(\lambda (H16: (eq C x2 (CHead x3 (Bind Void)
+x4))).(\lambda (H17: (csuba g x3 d1)).(let H18 \def (eq_ind C x2 (\lambda (c:
+C).(clear c2 c)) H13 (CHead x3 (Bind Void) x4) H16) in (or_intror (ex2 C
+(\lambda (d2: C).(getl O c2 (CHead d2 (Bind Abst) u))) (\lambda (d2:
+C).(csuba g d2 d1))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(getl O c2
+(CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2
+d1)))) (ex2_2_intro C T (\lambda (d2: C).(\lambda (u2: T).(getl O c2 (CHead
+d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))) x3
+x4 (getl_intro O c2 (CHead x3 (Bind Void) x4) c2 (drop_refl c2) H18)
+H17))))))) H15)) H14)))))) H11)))))))) (\lambda (n: nat).(\lambda (H8:
+((\forall (x1: C).((drop n O x1 (CHead x0 (Flat f) t)) \to (\forall (c2:
+C).((csuba g c2 x1) \to (or (ex2 C (\lambda (d2: C).(getl n c2 (CHead d2
+(Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1))) (ex2_2 C T (\lambda (d2:
+C).(\lambda (u2: T).(getl n c2 (CHead d2 (Bind Void) u2)))) (\lambda (d2:
+C).(\lambda (_: T).(csuba g d2 d1))))))))))).(\lambda (x1: C).(\lambda (H9:
+(drop (S n) O x1 (CHead x0 (Flat f) t))).(\lambda (c2: C).(\lambda (H10:
+(csuba g c2 x1)).(let H11 \def (drop_clear x1 (CHead x0 (Flat f) t) n H9) in
+(ex2_3_ind B C T (\lambda (b: B).(\lambda (e: C).(\lambda (v: T).(clear x1
+(CHead e (Bind b) v))))) (\lambda (_: B).(\lambda (e: C).(\lambda (_:
+T).(drop n O e (CHead x0 (Flat f) t))))) (or (ex2 C (\lambda (d2: C).(getl (S
+n) c2 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1))) (ex2_2 C
+T (\lambda (d2: C).(\lambda (u2: T).(getl (S n) c2 (CHead d2 (Bind Void)
+u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))) (\lambda (x2:
+B).(\lambda (x3: C).(\lambda (x4: T).(\lambda (H12: (clear x1 (CHead x3 (Bind
+x2) x4))).(\lambda (H13: (drop n O x3 (CHead x0 (Flat f) t))).(let H14 \def