-(THead (Bind b0) u t4) (asucc g a1))))))))) (\lambda (_: (ty3 g (CHead c0
-(Bind Abbr) u) t4 t0)).(\lambda (_: (ex2 A (\lambda (a1: A).(arity g (CHead
-c0 (Bind Abbr) u) t4 a1)) (\lambda (a1: A).(arity g (CHead c0 (Bind Abbr) u)
-t0 (asucc g a1))))).(\lambda (H16: (arity g (CHead c0 (Bind Abbr) u) t3
-x0)).(\lambda (H17: (arity g (CHead c0 (Bind Abbr) u) t4 (asucc g
-x0))).(ex_intro2 A (\lambda (a1: A).(arity g c0 (THead (Bind Abbr) u t3) a1))
-(\lambda (a1: A).(arity g c0 (THead (Bind Abbr) u t4) (asucc g a1))) x0
-(arity_bind g Abbr not_abbr_abst c0 u x H7 t3 x0 H16) (arity_bind g Abbr
-not_abbr_abst c0 u x H7 t4 (asucc g x0) H17)))))) (\lambda (_: (ty3 g (CHead
-c0 (Bind Abst) u) t4 t0)).(\lambda (_: (ex2 A (\lambda (a1: A).(arity g
-(CHead c0 (Bind Abst) u) t4 a1)) (\lambda (a1: A).(arity g (CHead c0 (Bind
-Abst) u) t0 (asucc g a1))))).(\lambda (H16: (arity g (CHead c0 (Bind Abst) u)
-t3 x0)).(\lambda (H17: (arity g (CHead c0 (Bind Abst) u) t4 (asucc g
-x0))).(ex_intro2 A (\lambda (a1: A).(arity g c0 (THead (Bind Abst) u t3) a1))
-(\lambda (a1: A).(arity g c0 (THead (Bind Abst) u t4) (asucc g a1))) (AHead
-x1 x0) (arity_head g c0 u x1 (arity_repl g c0 u x H7 (asucc g x1) H13) t3 x0
-H16) (arity_repl g c0 (THead (Bind Abst) u t4) (AHead x1 (asucc g x0))
-(arity_head g c0 u x1 (arity_repl g c0 u x H7 (asucc g x1) H13) t4 (asucc g
-x0) H17) (asucc g (AHead x1 x0)) (leq_refl g (asucc g (AHead x1 x0)))))))))
-(\lambda (_: (ty3 g (CHead c0 (Bind Void) u) t4 t0)).(\lambda (_: (ex2 A
-(\lambda (a1: A).(arity g (CHead c0 (Bind Void) u) t4 a1)) (\lambda (a1:
-A).(arity g (CHead c0 (Bind Void) u) t0 (asucc g a1))))).(\lambda (H16:
-(arity g (CHead c0 (Bind Void) u) t3 x0)).(\lambda (H17: (arity g (CHead c0
-(Bind Void) u) t4 (asucc g x0))).(ex_intro2 A (\lambda (a1: A).(arity g c0
-(THead (Bind Void) u t3) a1)) (\lambda (a1: A).(arity g c0 (THead (Bind Void)
-u t4) (asucc g a1))) x0 (arity_bind g Void not_void_abst c0 u x H7 t3 x0 H16)
-(arity_bind g Void not_void_abst c0 u x H7 t4 (asucc g x0) H17)))))) b H4 H5
-H10 H11))) H12)))))) H9))))) H6))))))))))))))) (\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) a1))
-(\lambda (a1: A).(arity g c0 (THead (Flat Appl) w (THead (Bind Abst) u t))
-(asucc g a1)))) (\lambda (x3: A).(\lambda (H16: (eq A x0 (AHead x1
+(THead (Bind b0) u t4) (asucc g a1))))))) (\lambda (H12: (arity g (CHead c0
+(Bind Abbr) u) t3 x0)).(\lambda (H13: (arity g (CHead c0 (Bind Abbr) u) t4
+(asucc g x0))).(ex_intro2 A (\lambda (a1: A).(arity g c0 (THead (Bind Abbr) u
+t3) a1)) (\lambda (a1: A).(arity g c0 (THead (Bind Abbr) u t4) (asucc g a1)))
+x0 (arity_bind g Abbr not_abbr_abst c0 u x H5 t3 x0 H12) (arity_bind g Abbr
+not_abbr_abst c0 u x H5 t4 (asucc g x0) H13)))) (\lambda (H12: (arity g
+(CHead c0 (Bind Abst) u) t3 x0)).(\lambda (H13: (arity g (CHead c0 (Bind
+Abst) u) t4 (asucc g x0))).(ex_intro2 A (\lambda (a1: A).(arity g c0 (THead
+(Bind Abst) u t3) a1)) (\lambda (a1: A).(arity g c0 (THead (Bind Abst) u t4)
+(asucc g a1))) (AHead x1 x0) (arity_head g c0 u x1 (arity_repl g c0 u x H5
+(asucc g x1) H11) t3 x0 H12) (arity_repl g c0 (THead (Bind Abst) u t4) (AHead
+x1 (asucc g x0)) (arity_head g c0 u x1 (arity_repl g c0 u x H5 (asucc g x1)
+H11) t4 (asucc g x0) H13) (asucc g (AHead x1 x0)) (leq_refl g (asucc g (AHead
+x1 x0))))))) (\lambda (H12: (arity g (CHead c0 (Bind Void) u) t3
+x0)).(\lambda (H13: (arity g (CHead c0 (Bind Void) u) t4 (asucc g
+x0))).(ex_intro2 A (\lambda (a1: A).(arity g c0 (THead (Bind Void) u t3) a1))
+(\lambda (a1: A).(arity g c0 (THead (Bind Void) u t4) (asucc g a1))) x0
+(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)
+a1)) (\lambda (a1: A).(arity g c0 (THead (Flat Appl) w (THead (Bind Abst) u
+t)) (asucc g a1)))) (\lambda (x3: A).(\lambda (H16: (eq A x0 (AHead x1