(S O))) H26)) in (ex_intro2 T (\lambda (x3: T).(subst1 i u t (lift (S O) i
x3))) (\lambda (x3: T).(pr2 a x1 x3)) x0 H27 (pr2_free a x1 x0 H10))))))
(subst1_confluence_eq t4 t u i (subst1_single i u t4 t H2) (lift (S O) i x0)
(S O))) H26)) in (ex_intro2 T (\lambda (x3: T).(subst1 i u t (lift (S O) i
x3))) (\lambda (x3: T).(pr2 a x1 x3)) x0 H27 (pr2_free a x1 x0 H10))))))
(subst1_confluence_eq t4 t u i (subst1_single i u t4 t H2) (lift (S O) i x0)