-(csubst1_getl_ge d0 i (le_S_n d0 i (le_S (S d0) i H12)) c0 a0 u0 H4 (CHead d
-(Bind Abbr) u) H0) a (S O) d0 H5 (eq_ind_r nat (plus (S O) d0) (\lambda (n:
-nat).(le n i)) H12 (plus d0 (S O)) (plus_sym d0 (S O)))) x1 x0 H10 x3
-H16)))))) (subst1_gen_lift_ge u x0 x2 i (S O) d0 H14 (eq_ind_r nat (plus (S
-O) d0) (\lambda (n: nat).(le n i)) H12 (plus d0 (S O)) (plus_sym d0 (S
-O)))))))) (subst1_confluence_neq t4 t u i (subst1_single i u t4 t H2) (lift
-(S O) d0 x0) u0 d0 H11 (sym_not_eq nat d0 i (lt_neq d0 i H12))))))))))
-(pr0_gen_lift x1 x (S O) d0 H7))))) (pr0_subst1 t3 t4 H1 u0 (lift (S O) d0
-x1) d0 H6 u0 (pr0_refl u0))))))))))))))))))))))) c t1 t2 H)))).
-(* COMMENTS
-Initial nodes: 3757
-END *)
+(csubst1_getl_ge d0 i (le_S_n d0 i (le_S_n (S d0) (S i) (le_S (S (S d0)) (S
+i) (le_n_S (S d0) i H12)))) c0 a0 u0 H4 (CHead d (Bind Abbr) u) H0) a (S O)
+d0 H5 (eq_ind_r nat (plus (S O) d0) (\lambda (n: nat).(le n i)) H12 (plus d0
+(S O)) (plus_sym d0 (S O)))) x1 x0 H10 x3 H16)))))) (subst1_gen_lift_ge u x0
+x2 i (S O) d0 H14 (eq_ind_r nat (plus (S O) d0) (\lambda (n: nat).(le n i))
+H12 (plus d0 (S O)) (plus_sym d0 (S O)))))))) (subst1_confluence_neq t4 t u i
+(subst1_single i u t4 t H2) (lift (S O) d0 x0) u0 d0 H11 (sym_not_eq nat d0 i
+(lt_neq d0 i H12)))))))))) (pr0_gen_lift x1 x (S O) d0 H7))))) (pr0_subst1 t3
+t4 H1 u0 (lift (S O) d0 x1) d0 H6 u0 (pr0_refl u0))))))))))))))))))))))) c t1
+t2 H)))).