-(arity_bind g Void not_void_abst c0 u x H5 t3 x0 H12) (arity_bind g Void
-not_void_abst c0 u x H5 t4 (asucc g x0) H13)))) b H8 H9))) H10)))))) H7)))))
-H4)))))))))))) (\lambda (c0: C).(\lambda (w: T).(\lambda (u: T).(\lambda (_:
-(ty3 g c0 w u)).(\lambda (H1: (ex2 A (\lambda (a1: A).(arity g c0 w a1))
-(\lambda (a1: A).(arity g c0 u (asucc g a1))))).(\lambda (v: T).(\lambda (t:
-T).(\lambda (_: (ty3 g c0 v (THead (Bind Abst) u t))).(\lambda (H3: (ex2 A
-(\lambda (a1: A).(arity g c0 v a1)) (\lambda (a1: A).(arity g c0 (THead (Bind
-Abst) u t) (asucc g a1))))).(let H4 \def H1 in (ex2_ind A (\lambda (a1:
-A).(arity g c0 w a1)) (\lambda (a1: A).(arity g c0 u (asucc g a1))) (ex2 A
-(\lambda (a1: A).(arity g c0 (THead (Flat Appl) w v) a1)) (\lambda (a1:
-A).(arity g c0 (THead (Flat Appl) w (THead (Bind Abst) u t)) (asucc g a1))))
-(\lambda (x: A).(\lambda (H5: (arity g c0 w x)).(\lambda (H6: (arity g c0 u
-(asucc g x))).(let H7 \def H3 in (ex2_ind A (\lambda (a1: A).(arity g c0 v
-a1)) (\lambda (a1: A).(arity g c0 (THead (Bind Abst) u t) (asucc g a1))) (ex2
-A (\lambda (a1: A).(arity g c0 (THead (Flat Appl) w v) a1)) (\lambda (a1:
-A).(arity g c0 (THead (Flat Appl) w (THead (Bind Abst) u t)) (asucc g a1))))
-(\lambda (x0: A).(\lambda (H8: (arity g c0 v x0)).(\lambda (H9: (arity g c0
-(THead (Bind Abst) u t) (asucc g x0))).(let H10 \def (arity_gen_abst g c0 u t
-(asucc g x0) H9) in (ex3_2_ind A A (\lambda (a1: A).(\lambda (a2: A).(eq A
-(asucc g x0) (AHead a1 a2)))) (\lambda (a1: A).(\lambda (_: A).(arity g c0 u
-(asucc g a1)))) (\lambda (_: A).(\lambda (a2: A).(arity g (CHead c0 (Bind
-Abst) u) t a2))) (ex2 A (\lambda (a1: A).(arity g c0 (THead (Flat Appl) w v)
+(arity_bind g Void (sym_not_eq B Abst Void not_abst_void) c0 u x H5 t3 x0
+H12) (arity_bind g Void (sym_not_eq B Abst Void not_abst_void) c0 u x H5 t4
+(asucc g x0) H13)))) b H8 H9))) H10)))))) H7))))) H4)))))))))))) (\lambda
+(c0: C).(\lambda (w: T).(\lambda (u: T).(\lambda (_: (ty3 g c0 w u)).(\lambda
+(H1: (ex2 A (\lambda (a1: A).(arity g c0 w a1)) (\lambda (a1: A).(arity g c0
+u (asucc g a1))))).(\lambda (v: T).(\lambda (t: T).(\lambda (_: (ty3 g c0 v
+(THead (Bind Abst) u t))).(\lambda (H3: (ex2 A (\lambda (a1: A).(arity g c0 v
+a1)) (\lambda (a1: A).(arity g c0 (THead (Bind Abst) u t) (asucc g
+a1))))).(let H4 \def H1 in (ex2_ind A (\lambda (a1: A).(arity g c0 w a1))
+(\lambda (a1: A).(arity g c0 u (asucc g a1))) (ex2 A (\lambda (a1: A).(arity
+g c0 (THead (Flat Appl) w v) a1)) (\lambda (a1: A).(arity g c0 (THead (Flat
+Appl) w (THead (Bind Abst) u t)) (asucc g a1)))) (\lambda (x: A).(\lambda
+(H5: (arity g c0 w x)).(\lambda (H6: (arity g c0 u (asucc g x))).(let H7 \def
+H3 in (ex2_ind A (\lambda (a1: A).(arity g c0 v a1)) (\lambda (a1: A).(arity
+g c0 (THead (Bind Abst) u t) (asucc g a1))) (ex2 A (\lambda (a1: A).(arity g
+c0 (THead (Flat Appl) w v) a1)) (\lambda (a1: A).(arity g c0 (THead (Flat
+Appl) w (THead (Bind Abst) u t)) (asucc g a1)))) (\lambda (x0: A).(\lambda
+(H8: (arity g c0 v x0)).(\lambda (H9: (arity g c0 (THead (Bind Abst) u t)
+(asucc g x0))).(let H10 \def (arity_gen_abst g c0 u t (asucc g x0) H9) in
+(ex3_2_ind A A (\lambda (a1: A).(\lambda (a2: A).(eq A (asucc g x0) (AHead a1
+a2)))) (\lambda (a1: A).(\lambda (_: A).(arity g c0 u (asucc g a1))))
+(\lambda (_: A).(\lambda (a2: A).(arity g (CHead c0 (Bind Abst) u) t a2)))
+(ex2 A (\lambda (a1: A).(arity g c0 (THead (Flat Appl) w v) a1)) (\lambda
+(a1: A).(arity g c0 (THead (Flat Appl) w (THead (Bind Abst) u t)) (asucc g
+a1)))) (\lambda (x1: A).(\lambda (x2: A).(\lambda (H11: (eq A (asucc g x0)
+(AHead x1 x2))).(\lambda (H12: (arity g c0 u (asucc g x1))).(\lambda (H13:
+(arity g (CHead c0 (Bind Abst) u) t x2)).(let H14 \def (sym_eq A (asucc g x0)
+(AHead x1 x2) H11) in (let H15 \def (asucc_gen_head g x1 x2 x0 H14) in
+(ex2_ind A (\lambda (a0: A).(eq A x0 (AHead x1 a0))) (\lambda (a0: A).(eq A
+x2 (asucc g a0))) (ex2 A (\lambda (a1: A).(arity g c0 (THead (Flat Appl) w v)