-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)))