-(\lambda (e: C).(match e in C return (\lambda (_: C).C) with [(CSort _)
-\Rightarrow d | (CHead c0 _ _) \Rightarrow c0])) (CHead d (Bind Abbr) u)
-(CHead d0 (Bind Abbr) u0) (getl_mono c (CHead d (Bind Abbr) u) i H (CHead d0
-(Bind Abbr) u0) H15)) in ((let H18 \def (f_equal C T (\lambda (e: C).(match e
-in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _ t)
-\Rightarrow t])) (CHead d (Bind Abbr) u) (CHead d0 (Bind Abbr) u0) (getl_mono
-c (CHead d (Bind Abbr) u) i H (CHead d0 (Bind Abbr) u0) H15)) in (\lambda
-(H19: (eq C d d0)).(let H20 \def (eq_ind_r T u0 (\lambda (t: T).(subst0 i t x
-x1)) H14 u H18) in (let H21 \def (eq_ind_r T u0 (\lambda (t: T).(getl i c
-(CHead d0 (Bind Abbr) t))) H16 u H18) in (let H22 \def (eq_ind_r C d0
-(\lambda (c0: C).(getl i c (CHead c0 (Bind Abbr) u))) H21 d H19) in (or4_ind
-(eq T x1 x0) (ex2 T (\lambda (t: T).(subst0 i u x1 t)) (\lambda (t:
-T).(subst0 i u x0 t))) (subst0 i u x1 x0) (subst0 i u x0 x1) (ex2 T (\lambda
-(t: T).(pr2 c t1 t)) (\lambda (t: T).(pr2 c t2 t))) (\lambda (H23: (eq T x1
-x0)).(let H24 \def (eq_ind T x1 (\lambda (t: T).(pr0 t2 t)) H11 x0 H23) in
-(ex_intro2 T (\lambda (t: T).(pr2 c t1 t)) (\lambda (t: T).(pr2 c t2 t)) x0
-(pr2_free c t1 x0 H8) (pr2_free c t2 x0 H24)))) (\lambda (H23: (ex2 T
-(\lambda (t: T).(subst0 i u x1 t)) (\lambda (t: T).(subst0 i u x0
-t)))).(ex2_ind T (\lambda (t: T).(subst0 i u x1 t)) (\lambda (t: T).(subst0 i
-u x0 t)) (ex2 T (\lambda (t: T).(pr2 c t1 t)) (\lambda (t: T).(pr2 c t2 t)))
-(\lambda (x2: T).(\lambda (H24: (subst0 i u x1 x2)).(\lambda (H25: (subst0 i
-u x0 x2)).(ex_intro2 T (\lambda (t: T).(pr2 c t1 t)) (\lambda (t: T).(pr2 c
-t2 t)) x2 (pr2_delta c d u i H22 t1 x0 H8 x2 H25) (pr2_delta c d u i H22 t2
-x1 H11 x2 H24))))) H23)) (\lambda (H23: (subst0 i u x1 x0)).(ex_intro2 T
-(\lambda (t: T).(pr2 c t1 t)) (\lambda (t: T).(pr2 c t2 t)) x0 (pr2_free c t1
-x0 H8) (pr2_delta c d u i H22 t2 x1 H11 x0 H23))) (\lambda (H23: (subst0 i u
-x0 x1)).(ex_intro2 T (\lambda (t: T).(pr2 c t1 t)) (\lambda (t: T).(pr2 c t2
-t)) x1 (pr2_delta c d u i H22 t1 x0 H8 x1 H23) (pr2_free c t2 x1 H11)))
-(subst0_confluence_eq x x1 u i H20 x0 H9))))))) H17)))))))))) H10))
-(pr0_subst0 t4 x H5 u0 t2 i0 H4 u0 (pr0_refl u0)))))) H7)) (pr0_subst0 t3 x
-H6 u t1 i H1 u (pr0_refl u)))))) (pr0_confluence t0 t4 H3 t3
-H0))))))))))))))))))).
-(* COMMENTS
-Initial nodes: 1901
-END *)
+(\lambda (e: C).(match e with [(CSort _) \Rightarrow d | (CHead c0 _ _)
+\Rightarrow c0])) (CHead d (Bind Abbr) u) (CHead d0 (Bind Abbr) u0)
+(getl_mono c (CHead d (Bind Abbr) u) i H (CHead d0 (Bind Abbr) u0) H15)) in
+((let H18 \def (f_equal C T (\lambda (e: C).(match e with [(CSort _)
+\Rightarrow u | (CHead _ _ t) \Rightarrow t])) (CHead d (Bind Abbr) u) (CHead
+d0 (Bind Abbr) u0) (getl_mono c (CHead d (Bind Abbr) u) i H (CHead d0 (Bind
+Abbr) u0) H15)) in (\lambda (H19: (eq C d d0)).(let H20 \def (eq_ind_r T u0
+(\lambda (t: T).(subst0 i t x x1)) H14 u H18) in (let H21 \def (eq_ind_r T u0
+(\lambda (t: T).(getl i c (CHead d0 (Bind Abbr) t))) H16 u H18) in (let H22
+\def (eq_ind_r C d0 (\lambda (c0: C).(getl i c (CHead c0 (Bind Abbr) u))) H21
+d H19) in (or4_ind (eq T x1 x0) (ex2 T (\lambda (t: T).(subst0 i u x1 t))
+(\lambda (t: T).(subst0 i u x0 t))) (subst0 i u x1 x0) (subst0 i u x0 x1)
+(ex2 T (\lambda (t: T).(pr2 c t1 t)) (\lambda (t: T).(pr2 c t2 t))) (\lambda
+(H23: (eq T x1 x0)).(let H24 \def (eq_ind T x1 (\lambda (t: T).(pr0 t2 t))
+H11 x0 H23) in (ex_intro2 T (\lambda (t: T).(pr2 c t1 t)) (\lambda (t:
+T).(pr2 c t2 t)) x0 (pr2_free c t1 x0 H8) (pr2_free c t2 x0 H24)))) (\lambda
+(H23: (ex2 T (\lambda (t: T).(subst0 i u x1 t)) (\lambda (t: T).(subst0 i u
+x0 t)))).(ex2_ind T (\lambda (t: T).(subst0 i u x1 t)) (\lambda (t:
+T).(subst0 i u x0 t)) (ex2 T (\lambda (t: T).(pr2 c t1 t)) (\lambda (t:
+T).(pr2 c t2 t))) (\lambda (x2: T).(\lambda (H24: (subst0 i u x1
+x2)).(\lambda (H25: (subst0 i u x0 x2)).(ex_intro2 T (\lambda (t: T).(pr2 c
+t1 t)) (\lambda (t: T).(pr2 c t2 t)) x2 (pr2_delta c d u i H22 t1 x0 H8 x2
+H25) (pr2_delta c d u i H22 t2 x1 H11 x2 H24))))) H23)) (\lambda (H23:
+(subst0 i u x1 x0)).(ex_intro2 T (\lambda (t: T).(pr2 c t1 t)) (\lambda (t:
+T).(pr2 c t2 t)) x0 (pr2_free c t1 x0 H8) (pr2_delta c d u i H22 t2 x1 H11 x0
+H23))) (\lambda (H23: (subst0 i u x0 x1)).(ex_intro2 T (\lambda (t: T).(pr2 c
+t1 t)) (\lambda (t: T).(pr2 c t2 t)) x1 (pr2_delta c d u i H22 t1 x0 H8 x1
+H23) (pr2_free c t2 x1 H11))) (subst0_confluence_eq x x1 u i H20 x0 H9)))))))
+H17)))))))))) H10)) (pr0_subst0 t4 x H5 u0 t2 i0 H4 u0 (pr0_refl u0))))))
+H7)) (pr0_subst0 t3 x H6 u t1 i H1 u (pr0_refl u)))))) (pr0_confluence t0 t4
+H3 t3 H0))))))))))))))))))).