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