u) e2)) x H5 (clear_flat c4 x H6 f u))))) H4)))) k H2))))))))) (\lambda (c3:
C).(\lambda (c4: C).(\lambda (H0: (csuba g c3 c4)).(\lambda (_: ((\forall
(e1: C).((clear c3 e1) \to (ex2 C (\lambda (e2: C).(csuba g e1 e2)) (\lambda
-(e2: C).(clear c4 e2))))))).(\lambda (t: T).(\lambda (a: A).(\lambda (H2:
-(arity g c3 t (asucc g a))).(\lambda (u: T).(\lambda (H3: (arity g c4 u
+(e2: C).(clear c4 e2))))))).(\lambda (b: B).(\lambda (H2: (not (eq B b
+Void))).(\lambda (u1: T).(\lambda (u2: T).(\lambda (e1: C).(\lambda (H3:
+(clear (CHead c3 (Bind Void) u1) e1)).(eq_ind_r C (CHead c3 (Bind Void) u1)
+(\lambda (c: C).(ex2 C (\lambda (e2: C).(csuba g c e2)) (\lambda (e2:
+C).(clear (CHead c4 (Bind b) u2) e2)))) (ex_intro2 C (\lambda (e2: C).(csuba
+g (CHead c3 (Bind Void) u1) e2)) (\lambda (e2: C).(clear (CHead c4 (Bind b)
+u2) e2)) (CHead c4 (Bind b) u2) (csuba_void g c3 c4 H0 b H2 u1 u2)
+(clear_bind b c4 u2)) e1 (clear_gen_bind Void c3 e1 u1 H3))))))))))))
+(\lambda (c3: C).(\lambda (c4: C).(\lambda (H0: (csuba g c3 c4)).(\lambda (_:
+((\forall (e1: C).((clear c3 e1) \to (ex2 C (\lambda (e2: C).(csuba g e1 e2))
+(\lambda (e2: C).(clear c4 e2))))))).(\lambda (t: T).(\lambda (a: A).(\lambda
+(H2: (arity g c3 t (asucc g a))).(\lambda (u: T).(\lambda (H3: (arity g c4 u
a)).(\lambda (e1: C).(\lambda (H4: (clear (CHead c3 (Bind Abst) t)
e1)).(eq_ind_r C (CHead c3 (Bind Abst) t) (\lambda (c: C).(ex2 C (\lambda
(e2: C).(csuba g c e2)) (\lambda (e2: C).(clear (CHead c4 (Bind Abbr) u)
u) e2)) x H5 (clear_flat c3 x H6 f u))))) H4)))) k H2))))))))) (\lambda (c3:
C).(\lambda (c4: C).(\lambda (H0: (csuba g c3 c4)).(\lambda (_: ((\forall
(e1: C).((clear c4 e1) \to (ex2 C (\lambda (e2: C).(csuba g e2 e1)) (\lambda
-(e2: C).(clear c3 e2))))))).(\lambda (t: T).(\lambda (a: A).(\lambda (H2:
-(arity g c3 t (asucc g a))).(\lambda (u: T).(\lambda (H3: (arity g c4 u
+(e2: C).(clear c3 e2))))))).(\lambda (b: B).(\lambda (H2: (not (eq B b
+Void))).(\lambda (u1: T).(\lambda (u2: T).(\lambda (e1: C).(\lambda (H3:
+(clear (CHead c4 (Bind b) u2) e1)).(eq_ind_r C (CHead c4 (Bind b) u2)
+(\lambda (c: C).(ex2 C (\lambda (e2: C).(csuba g e2 c)) (\lambda (e2:
+C).(clear (CHead c3 (Bind Void) u1) e2)))) (ex_intro2 C (\lambda (e2:
+C).(csuba g e2 (CHead c4 (Bind b) u2))) (\lambda (e2: C).(clear (CHead c3
+(Bind Void) u1) e2)) (CHead c3 (Bind Void) u1) (csuba_void g c3 c4 H0 b H2 u1
+u2) (clear_bind Void c3 u1)) e1 (clear_gen_bind b c4 e1 u2 H3))))))))))))
+(\lambda (c3: C).(\lambda (c4: C).(\lambda (H0: (csuba g c3 c4)).(\lambda (_:
+((\forall (e1: C).((clear c4 e1) \to (ex2 C (\lambda (e2: C).(csuba g e2 e1))
+(\lambda (e2: C).(clear c3 e2))))))).(\lambda (t: T).(\lambda (a: A).(\lambda
+(H2: (arity g c3 t (asucc g a))).(\lambda (u: T).(\lambda (H3: (arity g c4 u
a)).(\lambda (e1: C).(\lambda (H4: (clear (CHead c4 (Bind Abbr) u)
e1)).(eq_ind_r C (CHead c4 (Bind Abbr) u) (\lambda (c: C).(ex2 C (\lambda
(e2: C).(csuba g e2 c)) (\lambda (e2: C).(clear (CHead c3 (Bind Abst) t)