-u2))).(\lambda (H1: (pc3 c u1 u2)).(\lambda (P: Prop).(ex_ind T (\lambda (t0:
-T).(ty3 g (CHead c (Bind Abst) w) (lift (S O) O u2) t0)) P (\lambda (x:
-T).(\lambda (H2: (ty3 g (CHead c (Bind Abst) w) (lift (S O) O u2) x)).(let H3
-\def (ty3_gen_lift g (CHead c (Bind Abst) w) u2 x (S O) O H2 c (drop_drop
-(Bind Abst) O c c (drop_refl c) w)) in (ex2_ind T (\lambda (t2: T).(pc3
-(CHead c (Bind Abst) w) (lift (S O) O t2) x)) (\lambda (t2: T).(ty3 g c u2
-t2)) P (\lambda (x0: T).(\lambda (_: (pc3 (CHead c (Bind Abst) w) (lift (S O)
-O x0) x)).(\lambda (H5: (ty3 g c u2 x0)).(let H_y \def (ty3_conv g c u2 x0 H5
-(THead (Bind Abst) w t) u1 H H1) in (let H_x \def (ty3_arity g (CHead c (Bind
-Abst) w) t (lift (S O) O u2) H0) in (let H6 \def H_x in (ex2_ind A (\lambda
-(a1: A).(arity g (CHead c (Bind Abst) w) t a1)) (\lambda (a1: A).(arity g
-(CHead c (Bind Abst) w) (lift (S O) O u2) (asucc g a1))) P (\lambda (x1:
-A).(\lambda (H7: (arity g (CHead c (Bind Abst) w) t x1)).(\lambda (H8: (arity
-g (CHead c (Bind Abst) w) (lift (S O) O u2) (asucc g x1))).(let H_x0 \def
-(ty3_arity g c (THead (Bind Abst) w t) u2 H_y) in (let H9 \def H_x0 in
-(ex2_ind A (\lambda (a1: A).(arity g c (THead (Bind Abst) w t) a1)) (\lambda
-(a1: A).(arity g c u2 (asucc g a1))) P (\lambda (x2: A).(\lambda (H10: (arity
-g c (THead (Bind Abst) w t) x2)).(\lambda (H11: (arity g c u2 (asucc g
-x2))).(arity_repellent g c w t x1 H7 x2 H10 (asucc_inj g x1 x2 (arity_mono g
-c u2 (asucc g x1) (arity_gen_lift g (CHead c (Bind Abst) w) u2 (asucc g x1)
-(S O) O H8 c (drop_drop (Bind Abst) O c c (drop_refl c) w)) (asucc g x2)
-H11)) P)))) H9)))))) H6))))))) H3)))) (ty3_correct g (CHead c (Bind Abst) w)
-t (lift (S O) O u2) H0))))))))))).
-(* COMMENTS
-Initial nodes: 651
-END *)
+u2))).(\lambda (H1: (pc3 c u1 u2)).(\lambda (P: Prop).(let TMP_5 \def
+(\lambda (t0: T).(let TMP_1 \def (Bind Abst) in (let TMP_2 \def (CHead c
+TMP_1 w) in (let TMP_3 \def (S O) in (let TMP_4 \def (lift TMP_3 O u2) in
+(ty3 g TMP_2 TMP_4 t0)))))) in (let TMP_55 \def (\lambda (x: T).(\lambda (H2:
+(ty3 g (CHead c (Bind Abst) w) (lift (S O) O u2) x)).(let TMP_6 \def (Bind
+Abst) in (let TMP_7 \def (CHead c TMP_6 w) in (let TMP_8 \def (S O) in (let
+TMP_9 \def (Bind Abst) in (let TMP_10 \def (drop_refl c) in (let TMP_11 \def
+(drop_drop TMP_9 O c c TMP_10 w) in (let H3 \def (ty3_gen_lift g TMP_7 u2 x
+TMP_8 O H2 c TMP_11) in (let TMP_16 \def (\lambda (t2: T).(let TMP_12 \def
+(Bind Abst) in (let TMP_13 \def (CHead c TMP_12 w) in (let TMP_14 \def (S O)
+in (let TMP_15 \def (lift TMP_14 O t2) in (pc3 TMP_13 TMP_15 x)))))) in (let
+TMP_17 \def (\lambda (t2: T).(ty3 g c u2 t2)) in (let TMP_54 \def (\lambda
+(x0: T).(\lambda (_: (pc3 (CHead c (Bind Abst) w) (lift (S O) O x0)
+x)).(\lambda (H5: (ty3 g c u2 x0)).(let TMP_18 \def (Bind Abst) in (let
+TMP_19 \def (THead TMP_18 w t) in (let H_y \def (ty3_conv g c u2 x0 H5 TMP_19
+u1 H H1) in (let TMP_20 \def (Bind Abst) in (let TMP_21 \def (CHead c TMP_20
+w) in (let TMP_22 \def (S O) in (let TMP_23 \def (lift TMP_22 O u2) in (let
+H_x \def (ty3_arity g TMP_21 t TMP_23 H0) in (let H6 \def H_x in (let TMP_26
+\def (\lambda (a1: A).(let TMP_24 \def (Bind Abst) in (let TMP_25 \def (CHead
+c TMP_24 w) in (arity g TMP_25 t a1)))) in (let TMP_32 \def (\lambda (a1:
+A).(let TMP_27 \def (Bind Abst) in (let TMP_28 \def (CHead c TMP_27 w) in
+(let TMP_29 \def (S O) in (let TMP_30 \def (lift TMP_29 O u2) in (let TMP_31
+\def (asucc g a1) in (arity g TMP_28 TMP_30 TMP_31))))))) in (let TMP_53 \def
+(\lambda (x1: A).(\lambda (H7: (arity g (CHead c (Bind Abst) w) t
+x1)).(\lambda (H8: (arity g (CHead c (Bind Abst) w) (lift (S O) O u2) (asucc
+g x1))).(let TMP_33 \def (Bind Abst) in (let TMP_34 \def (THead TMP_33 w t)
+in (let H_x0 \def (ty3_arity g c TMP_34 u2 H_y) in (let H9 \def H_x0 in (let
+TMP_37 \def (\lambda (a1: A).(let TMP_35 \def (Bind Abst) in (let TMP_36 \def
+(THead TMP_35 w t) in (arity g c TMP_36 a1)))) in (let TMP_39 \def (\lambda
+(a1: A).(let TMP_38 \def (asucc g a1) in (arity g c u2 TMP_38))) in (let
+TMP_52 \def (\lambda (x2: A).(\lambda (H10: (arity g c (THead (Bind Abst) w
+t) x2)).(\lambda (H11: (arity g c u2 (asucc g x2))).(let TMP_40 \def (asucc g
+x1) in (let TMP_41 \def (Bind Abst) in (let TMP_42 \def (CHead c TMP_41 w) in
+(let TMP_43 \def (asucc g x1) in (let TMP_44 \def (S O) in (let TMP_45 \def
+(Bind Abst) in (let TMP_46 \def (drop_refl c) in (let TMP_47 \def (drop_drop
+TMP_45 O c c TMP_46 w) in (let TMP_48 \def (arity_gen_lift g TMP_42 u2 TMP_43
+TMP_44 O H8 c TMP_47) in (let TMP_49 \def (asucc g x2) in (let TMP_50 \def
+(arity_mono g c u2 TMP_40 TMP_48 TMP_49 H11) in (let TMP_51 \def (asucc_inj g
+x1 x2 TMP_50) in (arity_repellent g c w t x1 H7 x2 H10 TMP_51
+P)))))))))))))))) in (ex2_ind A TMP_37 TMP_39 P TMP_52 H9))))))))))) in
+(ex2_ind A TMP_26 TMP_32 P TMP_53 H6)))))))))))))))) in (ex2_ind T TMP_16
+TMP_17 P TMP_54 H3))))))))))))) in (let TMP_56 \def (Bind Abst) in (let
+TMP_57 \def (CHead c TMP_56 w) in (let TMP_58 \def (S O) in (let TMP_59 \def
+(lift TMP_58 O u2) in (let TMP_60 \def (ty3_correct g TMP_57 t TMP_59 H0) in
+(ex_ind T TMP_5 P TMP_55 TMP_60))))))))))))))))).