-(c3: C).(\lambda (w: T).(\lambda (a: A).(sc3 g a c3 w))))) (ex2 C (\lambda
-(e2: C).(drop (S n) O c2 e2)) (\lambda (e2: C).(csubc g e1 e2))) (\lambda
-(H4: (ex2 C (\lambda (c3: C).(eq C c2 (CHead c3 k t))) (\lambda (c3:
-C).(csubc g c c3)))).(ex2_ind C (\lambda (c3: C).(eq C c2 (CHead c3 k t)))
-(\lambda (c3: C).(csubc g c c3)) (ex2 C (\lambda (e2: C).(drop (S n) O c2
-e2)) (\lambda (e2: C).(csubc g e1 e2))) (\lambda (x: C).(\lambda (H5: (eq C
-c2 (CHead x k t))).(\lambda (H6: (csubc g c x)).(eq_ind_r C (CHead x k t)
-(\lambda (c0: C).(ex2 C (\lambda (e2: C).(drop (S n) O c0 e2)) (\lambda (e2:
-C).(csubc g e1 e2)))) (let H_x0 \def (H e1 (r k n) (drop_gen_drop k c e1 t n
-H1) x H6) in (let H7 \def H_x0 in (ex2_ind C (\lambda (e2: C).(drop (r k n) O
-x e2)) (\lambda (e2: C).(csubc g e1 e2)) (ex2 C (\lambda (e2: C).(drop (S n)
-O (CHead x k t) e2)) (\lambda (e2: C).(csubc g e1 e2))) (\lambda (x0:
-C).(\lambda (H8: (drop (r k n) O x x0)).(\lambda (H9: (csubc g e1
-x0)).(ex_intro2 C (\lambda (e2: C).(drop (S n) O (CHead x k t) e2)) (\lambda
-(e2: C).(csubc g e1 e2)) x0 (drop_drop k n x x0 H8 t) H9)))) H7))) c2 H5))))
-H4)) (\lambda (H4: (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 c2 (CHead c3 (Bind Abbr) w))))) (\lambda (c3: C).(\lambda (_:
-T).(\lambda (_: A).(csubc g c c3)))) (\lambda (_: C).(\lambda (_: T).(\lambda
-(a: A).(sc3 g (asucc g a) c t)))) (\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 c2 (CHead c3 (Bind Abbr) w))))) (\lambda (c3:
-C).(\lambda (_: T).(\lambda (_: A).(csubc g c c3)))) (\lambda (_: C).(\lambda
-(_: T).(\lambda (a: A).(sc3 g (asucc g a) c t)))) (\lambda (c3: C).(\lambda
-(w: T).(\lambda (a: A).(sc3 g a c3 w)))) (ex2 C (\lambda (e2: C).(drop (S n)
-O c2 e2)) (\lambda (e2: C).(csubc g e1 e2))) (\lambda (x0: C).(\lambda (x1:
-T).(\lambda (x2: A).(\lambda (H5: (eq K k (Bind Abst))).(\lambda (H6: (eq C
-c2 (CHead x0 (Bind Abbr) x1))).(\lambda (H7: (csubc g c x0)).(\lambda (_:
-(sc3 g (asucc g x2) c t)).(\lambda (_: (sc3 g x2 x0 x1)).(eq_ind_r C (CHead
-x0 (Bind Abbr) x1) (\lambda (c0: C).(ex2 C (\lambda (e2: C).(drop (S n) O c0
-e2)) (\lambda (e2: C).(csubc g e1 e2)))) (let H10 \def (eq_ind K k (\lambda
-(k0: K).(drop (r k0 n) O c e1)) (drop_gen_drop k c e1 t n H1) (Bind Abst) H5)
-in (let H11 \def (eq_ind K k (\lambda (k0: K).((drop n O (CHead c k0 t) e1)
-\to (\forall (c3: C).((csubc g (CHead c k0 t) c3) \to (ex2 C (\lambda (e2:
-C).(drop n O c3 e2)) (\lambda (e2: C).(csubc g e1 e2))))))) H0 (Bind Abst)
-H5) in (let H_x0 \def (H e1 (r (Bind Abst) n) H10 x0 H7) in (let H12 \def
-H_x0 in (ex2_ind C (\lambda (e2: C).(drop n O x0 e2)) (\lambda (e2: C).(csubc
-g e1 e2)) (ex2 C (\lambda (e2: C).(drop (S n) O (CHead x0 (Bind Abbr) x1)
-e2)) (\lambda (e2: C).(csubc g e1 e2))) (\lambda (x: C).(\lambda (H13: (drop
-n O x0 x)).(\lambda (H14: (csubc g e1 x)).(ex_intro2 C (\lambda (e2: C).(drop
-(S n) O (CHead x0 (Bind Abbr) x1) e2)) (\lambda (e2: C).(csubc g e1 e2)) x
-(drop_drop (Bind Abbr) n x0 x H13 x1) H14)))) H12))))) c2 H6))))))))) H4))
-H3)))))))) h))))))) c1)).
+(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 c2 (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 c c3)))))
+(ex2 C (\lambda (e2: C).(drop (S n) O c2 e2)) (\lambda (e2: C).(csubc g e1
+e2))) (\lambda (H4: (ex2 C (\lambda (c3: C).(eq C c2 (CHead c3 k t)))
+(\lambda (c3: C).(csubc g c c3)))).(ex2_ind C (\lambda (c3: C).(eq C c2
+(CHead c3 k t))) (\lambda (c3: C).(csubc g c c3)) (ex2 C (\lambda (e2:
+C).(drop (S n) O c2 e2)) (\lambda (e2: C).(csubc g e1 e2))) (\lambda (x:
+C).(\lambda (H5: (eq C c2 (CHead x k t))).(\lambda (H6: (csubc g c
+x)).(eq_ind_r C (CHead x k t) (\lambda (c0: C).(ex2 C (\lambda (e2: C).(drop
+(S n) O c0 e2)) (\lambda (e2: C).(csubc g e1 e2)))) (let H_x0 \def (H e1 (r k
+n) (drop_gen_drop k c e1 t n H1) x H6) in (let H7 \def H_x0 in (ex2_ind C
+(\lambda (e2: C).(drop (r k n) O x e2)) (\lambda (e2: C).(csubc g e1 e2))
+(ex2 C (\lambda (e2: C).(drop (S n) O (CHead x k t) e2)) (\lambda (e2:
+C).(csubc g e1 e2))) (\lambda (x0: C).(\lambda (H8: (drop (r k n) O x
+x0)).(\lambda (H9: (csubc g e1 x0)).(ex_intro2 C (\lambda (e2: C).(drop (S n)
+O (CHead x k t) e2)) (\lambda (e2: C).(csubc g e1 e2)) x0 (drop_drop k n x x0
+H8 t) H9)))) H7))) c2 H5)))) H4)) (\lambda (H4: (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 c2 (CHead c3 (Bind Abbr) w)))))
+(\lambda (c3: C).(\lambda (_: T).(\lambda (_: A).(csubc g c c3)))) (\lambda
+(_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g (asucc g a) c t)))) (\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 c2 (CHead c3 (Bind
+Abbr) w))))) (\lambda (c3: C).(\lambda (_: T).(\lambda (_: A).(csubc g c
+c3)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g (asucc g a) c
+t)))) (\lambda (c3: C).(\lambda (w: T).(\lambda (a: A).(sc3 g a c3 w)))) (ex2
+C (\lambda (e2: C).(drop (S n) O c2 e2)) (\lambda (e2: C).(csubc g e1 e2)))
+(\lambda (x0: C).(\lambda (x1: T).(\lambda (x2: A).(\lambda (H5: (eq K k
+(Bind Abst))).(\lambda (H6: (eq C c2 (CHead x0 (Bind Abbr) x1))).(\lambda
+(H7: (csubc g c x0)).(\lambda (_: (sc3 g (asucc g x2) c t)).(\lambda (_: (sc3
+g x2 x0 x1)).(eq_ind_r C (CHead x0 (Bind Abbr) x1) (\lambda (c0: C).(ex2 C
+(\lambda (e2: C).(drop (S n) O c0 e2)) (\lambda (e2: C).(csubc g e1 e2))))
+(let H10 \def (eq_ind K k (\lambda (k0: K).(drop (r k0 n) O c e1))
+(drop_gen_drop k c e1 t n H1) (Bind Abst) H5) in (let H11 \def (eq_ind K k
+(\lambda (k0: K).((drop n O (CHead c k0 t) e1) \to (\forall (c3: C).((csubc g
+(CHead c k0 t) c3) \to (ex2 C (\lambda (e2: C).(drop n O c3 e2)) (\lambda
+(e2: C).(csubc g e1 e2))))))) H0 (Bind Abst) H5) in (let H_x0 \def (H e1 (r
+(Bind Abst) n) H10 x0 H7) in (let H12 \def H_x0 in (ex2_ind C (\lambda (e2:
+C).(drop n O x0 e2)) (\lambda (e2: C).(csubc g e1 e2)) (ex2 C (\lambda (e2:
+C).(drop (S n) O (CHead x0 (Bind Abbr) x1) e2)) (\lambda (e2: C).(csubc g e1
+e2))) (\lambda (x: C).(\lambda (H13: (drop n O x0 x)).(\lambda (H14: (csubc g
+e1 x)).(ex_intro2 C (\lambda (e2: C).(drop (S n) O (CHead x0 (Bind Abbr) x1)
+e2)) (\lambda (e2: C).(csubc g e1 e2)) x (drop_drop (Bind Abbr) n x0 x H13
+x1) H14)))) H12))))) c2 H6))))))))) H4)) (\lambda (H4: (ex4_3 B C T (\lambda
+(b: B).(\lambda (c3: C).(\lambda (v2: T).(eq C c2 (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 c
+c3)))))).(ex4_3_ind B C T (\lambda (b: B).(\lambda (c3: C).(\lambda (v2:
+T).(eq C c2 (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 c c3)))) (ex2 C (\lambda (e2: C).(drop (S n) O c2
+e2)) (\lambda (e2: C).(csubc g e1 e2))) (\lambda (x0: B).(\lambda (x1:
+C).(\lambda (x2: T).(\lambda (H5: (eq C c2 (CHead x1 (Bind x0) x2))).(\lambda
+(H6: (eq K k (Bind Void))).(\lambda (_: (not (eq B x0 Void))).(\lambda (H8:
+(csubc g c x1)).(eq_ind_r C (CHead x1 (Bind x0) x2) (\lambda (c0: C).(ex2 C
+(\lambda (e2: C).(drop (S n) O c0 e2)) (\lambda (e2: C).(csubc g e1 e2))))
+(let H9 \def (eq_ind K k (\lambda (k0: K).(drop (r k0 n) O c e1))
+(drop_gen_drop k c e1 t n H1) (Bind Void) H6) in (let H10 \def (eq_ind K k
+(\lambda (k0: K).((drop n O (CHead c k0 t) e1) \to (\forall (c3: C).((csubc g
+(CHead c k0 t) c3) \to (ex2 C (\lambda (e2: C).(drop n O c3 e2)) (\lambda
+(e2: C).(csubc g e1 e2))))))) H0 (Bind Void) H6) in (let H_x0 \def (H e1 (r
+(Bind Void) n) H9 x1 H8) in (let H11 \def H_x0 in (ex2_ind C (\lambda (e2:
+C).(drop n O x1 e2)) (\lambda (e2: C).(csubc g e1 e2)) (ex2 C (\lambda (e2:
+C).(drop (S n) O (CHead x1 (Bind x0) x2) e2)) (\lambda (e2: C).(csubc g e1
+e2))) (\lambda (x: C).(\lambda (H12: (drop n O x1 x)).(\lambda (H13: (csubc g
+e1 x)).(ex_intro2 C (\lambda (e2: C).(drop (S n) O (CHead x1 (Bind x0) x2)
+e2)) (\lambda (e2: C).(csubc g e1 e2)) x (drop_drop (Bind x0) n x1 x H12 x2)
+H13)))) H11))))) c2 H5)))))))) H4)) H3)))))))) h))))))) c1)).