-(ex2_ind C (\lambda (d2: C).(eq C c2 (CHead d2 (Bind Abst) t))) (\lambda (d2:
-C).(csuba g d2 c)) (ex2 C (\lambda (d2: C).(drop (S n) O c2 (CHead d2 (Bind
-Abst) u))) (\lambda (d2: C).(csuba g d2 d1))) (\lambda (x: C).(\lambda (H8:
-(eq C c2 (CHead x (Bind Abst) t))).(\lambda (H9: (csuba g x c)).(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 Abst) u))) (\lambda (d2: C).(csuba g d2 d1)))) (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 Abst) u))) (\lambda (d2: C).(csuba g d2 d1)) (ex2 C (\lambda (d2:
-C).(drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Abst) u))) (\lambda
-(d2: C).(csuba g d2 d1))) (\lambda (x0: C).(\lambda (H11: (drop n O x (CHead
-x0 (Bind Abst) u))).(\lambda (H12: (csuba g x0 d1)).(let H13 \def (refl_equal
-nat (r (Bind Abst) n)) in (let H14 \def (eq_ind nat n (\lambda (n0:
-nat).(drop n0 O x (CHead x0 (Bind Abst) u))) H11 (r (Bind Abst) n) H13) in
-(ex_intro2 C (\lambda (d2: C).(drop (S n) O (CHead x (Bind Abst) t) (CHead d2
-(Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1)) x0 (drop_drop (Bind Abst)
-n x (CHead x0 (Bind Abst) u) H14 t) H12)))))) H10)) c2 H8)))) H7)))))
-(\lambda (H5: (csuba g c2 (CHead c (Bind Void) t))).(\lambda (H6: (drop (r
-(Bind Void) n) O c (CHead d1 (Bind Abst) u))).(let H_x \def
-(csuba_gen_void_rev g c c2 t H5) in (let H7 \def H_x in (ex2_ind C (\lambda
-(d2: C).(eq C c2 (CHead d2 (Bind Void) t))) (\lambda (d2: C).(csuba g d2 c))
-(ex2 C (\lambda (d2: C).(drop (S n) O c2 (CHead d2 (Bind Abst) u))) (\lambda
-(d2: C).(csuba g d2 d1))) (\lambda (x: C).(\lambda (H8: (eq C c2 (CHead x
-(Bind Void) t))).(\lambda (H9: (csuba g x c)).(eq_ind_r C (CHead x (Bind
-Void) t) (\lambda (c0: C).(ex2 C (\lambda (d2: C).(drop (S n) O c0 (CHead d2
-(Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1)))) (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 Abst)
-u))) (\lambda (d2: C).(csuba g d2 d1)) (ex2 C (\lambda (d2: C).(drop (S n) O
-(CHead x (Bind Void) t) (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g
-d2 d1))) (\lambda (x0: C).(\lambda (H11: (drop n O x (CHead x0 (Bind Abst)
-u))).(\lambda (H12: (csuba g x0 d1)).(let H13 \def (refl_equal nat (r (Bind
-Abst) n)) in (let H14 \def (eq_ind nat n (\lambda (n0: nat).(drop n0 O x
-(CHead x0 (Bind Abst) u))) H11 (r (Bind Abst) n) H13) in (ex_intro2 C
+(or_ind (ex2 C (\lambda (d2: C).(eq C c2 (CHead d2 (Bind Abst) t))) (\lambda
+(d2: C).(csuba g d2 c))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq C
+c2 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2
+c)))) (or (ex2 C (\lambda (d2: C).(drop (S n) 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 (S n) O c2 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda
+(_: T).(csuba g d2 d1))))) (\lambda (H8: (ex2 C (\lambda (d2: C).(eq C c2
+(CHead d2 (Bind Abst) t))) (\lambda (d2: C).(csuba g d2 c)))).(ex2_ind C
+(\lambda (d2: C).(eq C c2 (CHead d2 (Bind Abst) t))) (\lambda (d2: C).(csuba
+g d2 c)) (or (ex2 C (\lambda (d2: C).(drop (S n) 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 (S n) O c2 (CHead d2 (Bind Void) u2)))) (\lambda (d2:
+C).(\lambda (_: T).(csuba g d2 d1))))) (\lambda (x: C).(\lambda (H9: (eq C c2
+(CHead x (Bind Abst) t))).(\lambda (H10: (csuba g x c)).(eq_ind_r C (CHead x
+(Bind Abst) t) (\lambda (c0: C).(or (ex2 C (\lambda (d2: C).(drop (S n) O c0
+(CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1))) (ex2_2 C T
+(\lambda (d2: C).(\lambda (u2: T).(drop (S n) O c0 (CHead d2 (Bind Void)
+u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1)))))) (let H11 \def (H
+c d1 u H6 g x H10) in (or_ind (ex2 C (\lambda (d2: C).(drop n O x (CHead d2
+(Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1))) (ex2_2 C T (\lambda (d2:
+C).(\lambda (u2: T).(drop n O x (CHead d2 (Bind Void) u2)))) (\lambda (d2:
+C).(\lambda (_: T).(csuba g d2 d1)))) (or (ex2 C (\lambda (d2: C).(drop (S n)
+O (CHead x (Bind Abst) t) (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba
+g d2 d1))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(drop (S n) O (CHead
+x (Bind Abst) t) (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_:
+T).(csuba g d2 d1))))) (\lambda (H12: (ex2 C (\lambda (d2: C).(drop n O x
+(CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1)))).(ex2_ind C
+(\lambda (d2: C).(drop n O x (CHead d2 (Bind Abst) u))) (\lambda (d2:
+C).(csuba g d2 d1)) (or (ex2 C (\lambda (d2: C).(drop (S n) O (CHead x (Bind
+Abst) t) (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1))) (ex2_2
+C T (\lambda (d2: C).(\lambda (u2: T).(drop (S n) O (CHead x (Bind Abst) t)
+(CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2
+d1))))) (\lambda (x0: C).(\lambda (H13: (drop n O x (CHead x0 (Bind Abst)
+u))).(\lambda (H14: (csuba g x0 d1)).(or_introl (ex2 C (\lambda (d2: C).(drop
+(S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Abst) u))) (\lambda (d2:
+C).(csuba g d2 d1))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(drop (S n)
+O (CHead x (Bind Abst) t) (CHead d2 (Bind Void) u2)))) (\lambda (d2:
+C).(\lambda (_: T).(csuba g d2 d1)))) (ex_intro2 C (\lambda (d2: C).(drop (S
+n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Abst) u))) (\lambda (d2:
+C).(csuba g d2 d1)) x0 (drop_drop (Bind Abst) n x (CHead x0 (Bind Abst) u)
+H13 t) H14))))) H12)) (\lambda (H12: (ex2_2 C T (\lambda (d2: C).(\lambda
+(u2: T).(drop n O x (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 n O x (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_:
+T).(csuba g d2 d1))) (or (ex2 C (\lambda (d2: C).(drop (S n) O (CHead x (Bind
+Abst) t) (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1))) (ex2_2
+C T (\lambda (d2: C).(\lambda (u2: T).(drop (S n) O (CHead x (Bind Abst) t)
+(CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2
+d1))))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H13: (drop n O x (CHead
+x0 (Bind Void) x1))).(\lambda (H14: (csuba g x0 d1)).(or_intror (ex2 C
+(\lambda (d2: C).(drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Abst)
+u))) (\lambda (d2: C).(csuba g d2 d1))) (ex2_2 C T (\lambda (d2: C).(\lambda
+(u2: T).(drop (S n) O (CHead x (Bind Abst) t) (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).(drop (S n) O (CHead x (Bind Abst) t) (CHead d2
+(Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))) x0 x1
+(drop_drop (Bind Abst) n x (CHead x0 (Bind Void) x1) H13 t) H14)))))) H12))
+H11)) c2 H9)))) H8)) (\lambda (H8: (ex2_2 C T (\lambda (d2: C).(\lambda (u2:
+T).(eq C c2 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_:
+T).(csuba g d2 c))))).(ex2_2_ind C T (\lambda (d2: C).(\lambda (u2: T).(eq C
+c2 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2
+c))) (or (ex2 C (\lambda (d2: C).(drop (S n) 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 (S n) O c2 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda
+(_: T).(csuba g d2 d1))))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H9:
+(eq C c2 (CHead x0 (Bind Void) x1))).(\lambda (H10: (csuba g x0 c)).(eq_ind_r
+C (CHead x0 (Bind Void) x1) (\lambda (c0: C).(or (ex2 C (\lambda (d2:
+C).(drop (S n) O c0 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2
+d1))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(drop (S n) O c0 (CHead d2
+(Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1)))))) (let
+H11 \def (H c d1 u H6 g x0 H10) in (or_ind (ex2 C (\lambda (d2: C).(drop n O
+x0 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1))) (ex2_2 C T
+(\lambda (d2: C).(\lambda (u2: T).(drop n O x0 (CHead d2 (Bind Void) u2))))
+(\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1)))) (or (ex2 C (\lambda (d2:
+C).(drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Abst) u)))
+(\lambda (d2: C).(csuba g d2 d1))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2:
+T).(drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Void) u2))))
+(\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))) (\lambda (H12: (ex2 C
+(\lambda (d2: C).(drop n O x0 (CHead d2 (Bind Abst) u))) (\lambda (d2:
+C).(csuba g d2 d1)))).(ex2_ind C (\lambda (d2: C).(drop n O x0 (CHead d2
+(Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1)) (or (ex2 C (\lambda (d2:
+C).(drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Abst) u)))
+(\lambda (d2: C).(csuba g d2 d1))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2:
+T).(drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Void) u2))))
+(\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))) (\lambda (x: C).(\lambda
+(H13: (drop n O x0 (CHead x (Bind Abst) u))).(\lambda (H14: (csuba g x
+d1)).(or_introl (ex2 C (\lambda (d2: C).(drop (S n) O (CHead x0 (Bind Void)
+x1) (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1))) (ex2_2 C T
+(\lambda (d2: C).(\lambda (u2: T).(drop (S n) O (CHead x0 (Bind Void) x1)
+(CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2
+d1)))) (ex_intro2 C (\lambda (d2: C).(drop (S n) O (CHead x0 (Bind Void) x1)
+(CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1)) x (drop_drop
+(Bind Void) n x0 (CHead x (Bind Abst) u) H13 x1) H14))))) H12)) (\lambda
+(H12: (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(drop n O x0 (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 n O x0 (CHead
+d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))) (or
+(ex2 C (\lambda (d2: C).(drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2
+(Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1))) (ex2_2 C T (\lambda (d2:
+C).(\lambda (u2: T).(drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind
+Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))) (\lambda
+(x2: C).(\lambda (x3: T).(\lambda (H13: (drop n O x0 (CHead x2 (Bind Void)
+x3))).(\lambda (H14: (csuba g x2 d1)).(or_intror (ex2 C (\lambda (d2:
+C).(drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2 (Bind Abst) u)))
+(\lambda (d2: C).(csuba g d2 d1))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2:
+T).(drop (S n) O (CHead x0 (Bind Void) x1) (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).(drop (S n) O (CHead x0 (Bind Void) x1) (CHead d2
+(Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))) x2 x3
+(drop_drop (Bind Void) n x0 (CHead x2 (Bind Void) x3) H13 x1) H14)))))) H12))
+H11)) c2 H9))))) H8)) H7))))) (\lambda (H5: (csuba g c2 (CHead c (Bind Void)
+t))).(\lambda (H6: (drop (r (Bind Void) n) O c (CHead d1 (Bind Abst)
+u))).(let H_x \def (csuba_gen_void_rev g c c2 t H5) in (let H7 \def H_x in
+(ex2_ind C (\lambda (d2: C).(eq C c2 (CHead d2 (Bind Void) t))) (\lambda (d2:
+C).(csuba g d2 c)) (or (ex2 C (\lambda (d2: C).(drop (S n) 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 (S n) O c2 (CHead d2 (Bind Void) u2)))) (\lambda
+(d2: C).(\lambda (_: T).(csuba g d2 d1))))) (\lambda (x: C).(\lambda (H8: (eq
+C c2 (CHead x (Bind Void) t))).(\lambda (H9: (csuba g x c)).(eq_ind_r C
+(CHead x (Bind Void) t) (\lambda (c0: C).(or (ex2 C (\lambda (d2: C).(drop (S
+n) O c0 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1))) (ex2_2
+C T (\lambda (d2: C).(\lambda (u2: T).(drop (S n) O c0 (CHead d2 (Bind Void)
+u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1)))))) (let H10 \def (H
+c d1 u H6 g x H9) in (or_ind (ex2 C (\lambda (d2: C).(drop n O x (CHead d2
+(Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1))) (ex2_2 C T (\lambda (d2:
+C).(\lambda (u2: T).(drop n O x (CHead d2 (Bind Void) u2)))) (\lambda (d2:
+C).(\lambda (_: T).(csuba g d2 d1)))) (or (ex2 C (\lambda (d2: C).(drop (S n)
+O (CHead x (Bind Void) t) (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba
+g d2 d1))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(drop (S n) O (CHead
+x (Bind Void) t) (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_:
+T).(csuba g d2 d1))))) (\lambda (H11: (ex2 C (\lambda (d2: C).(drop n O x
+(CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1)))).(ex2_ind C
+(\lambda (d2: C).(drop n O x (CHead d2 (Bind Abst) u))) (\lambda (d2:
+C).(csuba g d2 d1)) (or (ex2 C (\lambda (d2: C).(drop (S n) O (CHead x (Bind
+Void) t) (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1))) (ex2_2
+C T (\lambda (d2: C).(\lambda (u2: T).(drop (S n) O (CHead x (Bind Void) t)
+(CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2
+d1))))) (\lambda (x0: C).(\lambda (H12: (drop n O x (CHead x0 (Bind Abst)
+u))).(\lambda (H13: (csuba g x0 d1)).(or_introl (ex2 C (\lambda (d2: C).(drop
+(S n) O (CHead x (Bind Void) t) (CHead d2 (Bind Abst) u))) (\lambda (d2:
+C).(csuba g d2 d1))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(drop (S n)
+O (CHead x (Bind Void) t) (CHead d2 (Bind Void) u2)))) (\lambda (d2:
+C).(\lambda (_: T).(csuba g d2 d1)))) (ex_intro2 C (\lambda (d2: C).(drop (S
+n) O (CHead x (Bind Void) t) (CHead d2 (Bind Abst) u))) (\lambda (d2:
+C).(csuba g d2 d1)) x0 (drop_drop (Bind Void) n x (CHead x0 (Bind Abst) u)
+H12 t) H13))))) H11)) (\lambda (H11: (ex2_2 C T (\lambda (d2: C).(\lambda
+(u2: T).(drop n O x (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 n O x (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_:
+T).(csuba g d2 d1))) (or (ex2 C (\lambda (d2: C).(drop (S n) O (CHead x (Bind
+Void) t) (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1))) (ex2_2
+C T (\lambda (d2: C).(\lambda (u2: T).(drop (S n) O (CHead x (Bind Void) t)
+(CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2
+d1))))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H12: (drop n O x (CHead
+x0 (Bind Void) x1))).(\lambda (H13: (csuba g x0 d1)).(or_intror (ex2 C