-(CHead c1 k u))).(let H9 \def (eq_ind C c (\lambda (c0: C).(getl i c0 (CHead
-d (Bind Abbr) u0))) H5 (CHead c1 k u) H8) in (ex3_2_ind C T (\lambda (e2:
-C).(\lambda (u2: T).(getl i (CHead c2 k u) (CHead e2 (Bind Abbr) u2))))
-(\lambda (e2: C).(\lambda (_: T).(wcpr0 d e2))) (\lambda (_: C).(\lambda (u2:
-T).(pr0 u0 u2))) (pc3 (CHead c2 k u) t6 t) (\lambda (x0: C).(\lambda (x1:
-T).(\lambda (H10: (getl i (CHead c2 k u) (CHead x0 (Bind Abbr) x1))).(\lambda
-(_: (wcpr0 d x0)).(\lambda (H12: (pr0 u0 x1)).(ex2_ind T (\lambda (t7:
-T).(subst0 i x1 t0 t7)) (\lambda (t7: T).(pr0 t t7)) (pc3 (CHead c2 k u) t6
-t) (\lambda (x: T).(\lambda (H13: (subst0 i x1 t0 x)).(\lambda (H14: (pr0 t
-x)).(pc3_pr2_u (CHead c2 k u) x t6 (pr2_delta (CHead c2 k u) x0 x1 i H10 t6
-t0 H6 x H13) t (pc3_pr2_x (CHead c2 k u) x t (pr2_free (CHead c2 k u) t x
-H14)))))) (pr0_subst0_fwd u0 t0 t i H7 x1 H12))))))) (wcpr0_getl (CHead c1 k
-u) (CHead c2 k u) (wcpr0_comp c1 c2 H u u (pr0_refl u) k) i d u0 (Bind Abbr)
-H9)))))))))))))) y t4 t3 H4))) H1) t5 H3))))))) t1 t2 H0)))))))).
-(* COMMENTS
-Initial nodes: 689
-END *)
+(CHead c1 k u))).(let TMP_19 \def (\lambda (c0: C).(let TMP_17 \def (Bind
+Abbr) in (let TMP_18 \def (CHead d TMP_17 u0) in (getl i c0 TMP_18)))) in
+(let TMP_20 \def (CHead c1 k u) in (let H9 \def (eq_ind C c TMP_19 H5 TMP_20
+H8) in (let TMP_24 \def (\lambda (e2: C).(\lambda (u2: T).(let TMP_21 \def
+(CHead c2 k u) in (let TMP_22 \def (Bind Abbr) in (let TMP_23 \def (CHead e2
+TMP_22 u2) in (getl i TMP_21 TMP_23)))))) in (let TMP_25 \def (\lambda (e2:
+C).(\lambda (_: T).(wcpr0 d e2))) in (let TMP_26 \def (\lambda (_:
+C).(\lambda (u2: T).(pr0 u0 u2))) in (let TMP_27 \def (CHead c2 k u) in (let
+TMP_28 \def (pc3 TMP_27 t6 t) in (let TMP_42 \def (\lambda (x0: C).(\lambda
+(x1: T).(\lambda (H10: (getl i (CHead c2 k u) (CHead x0 (Bind Abbr)
+x1))).(\lambda (_: (wcpr0 d x0)).(\lambda (H12: (pr0 u0 x1)).(let TMP_29 \def
+(\lambda (t7: T).(subst0 i x1 t0 t7)) in (let TMP_30 \def (\lambda (t7:
+T).(pr0 t t7)) in (let TMP_31 \def (CHead c2 k u) in (let TMP_32 \def (pc3
+TMP_31 t6 t) in (let TMP_40 \def (\lambda (x: T).(\lambda (H13: (subst0 i x1
+t0 x)).(\lambda (H14: (pr0 t x)).(let TMP_33 \def (CHead c2 k u) in (let
+TMP_34 \def (CHead c2 k u) in (let TMP_35 \def (pr2_delta TMP_34 x0 x1 i H10
+t6 t0 H6 x H13) in (let TMP_36 \def (CHead c2 k u) in (let TMP_37 \def (CHead
+c2 k u) in (let TMP_38 \def (pr2_free TMP_37 t x H14) in (let TMP_39 \def
+(pc3_pr2_x TMP_36 x t TMP_38) in (pc3_pr2_u TMP_33 x t6 TMP_35 t
+TMP_39))))))))))) in (let TMP_41 \def (pr0_subst0_fwd u0 t0 t i H7 x1 H12) in
+(ex2_ind T TMP_29 TMP_30 TMP_32 TMP_40 TMP_41)))))))))))) in (let TMP_43 \def
+(CHead c1 k u) in (let TMP_44 \def (CHead c2 k u) in (let TMP_45 \def
+(pr0_refl u) in (let TMP_46 \def (wcpr0_comp c1 c2 H u u TMP_45 k) in (let
+TMP_47 \def (Bind Abbr) in (let TMP_48 \def (wcpr0_getl TMP_43 TMP_44 TMP_46
+i d u0 TMP_47 H9) in (ex3_2_ind C T TMP_24 TMP_25 TMP_26 TMP_28 TMP_42
+TMP_48))))))))))))))))))))))))))) in (pr2_ind TMP_12 TMP_16 TMP_49 y t4 t3
+H4)))))) in (let TMP_51 \def (insert_eq C TMP_7 TMP_8 TMP_10 TMP_50 H1) in
+(pc3_t t3 TMP_6 t4 TMP_51 t5 H3))))))))))))) in (pr3_ind TMP_1 TMP_3 TMP_5
+TMP_52 t1 t2 H0)))))))))))).