(eq_ind_r nat (plus (S O) i) (\lambda (n: nat).(lt i n)) (le_n (plus (S O)
i)) (plus i (S O)) (plus_sym i (S O))) H1 (eq T t1 t2)))
(subst0_confluence_eq t0 (lift (S O) i t2) u i H0 (lift (S O) i t1) H)))))))).
(eq_ind_r nat (plus (S O) i) (\lambda (n: nat).(lt i n)) (le_n (plus (S O)
i)) (plus i (S O)) (plus_sym i (S O))) H1 (eq T t1 t2)))
(subst0_confluence_eq t0 (lift (S O) i t2) u i H0 (lift (S O) i t1) H)))))))).