(pr0 t0 x)).(\lambda (H5: (subst0 i v2 t2 x)).(ex_intro2 T (\lambda (w2:
T).(pr0 t0 w2)) (\lambda (w2: T).(subst1 i v2 t2 w2)) x H4 (subst1_single i
v2 t2 x H5))))) H3)) (pr0_subst0 t1 t2 H v1 t0 i H1 v2 H2)))))) w1 H0))))))).
(pr0 t0 x)).(\lambda (H5: (subst0 i v2 t2 x)).(ex_intro2 T (\lambda (w2:
T).(pr0 t0 w2)) (\lambda (w2: T).(subst1 i v2 t2 w2)) x H4 (subst1_single i
v2 t2 x H5))))) H3)) (pr0_subst0 t1 t2 H v1 t0 i H1 v2 H2)))))) w1 H0))))))).