x2)).(\lambda (H26: (subst1 i u (lift (S O) i x0) x2)).(let H27 \def (eq_ind
T x2 (\lambda (t0: T).(subst1 i u t t0)) H25 (lift (S O) i x0)
(subst1_gen_lift_eq x0 u x2 (S O) i i (le_n i) (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_comm i
+(\lambda (n: nat).(lt i n)) (le_n (plus (S O) i)) (plus i (S O)) (plus_sym i
(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)
(minus i (S O)) (getl_drop_conf_ge i (CHead d (Bind Abbr) u) a0
(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_comm d0 (S O)))) x1 x0 H10 x3
+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_comm d0 (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