x0)).(ex_intro2 T (\lambda (t: T).(pr1 t4 t)) (\lambda (t: T).(pr1 t5 t)) x0
H7 (pr1_t x t5 (pr1_pr0 t5 x H4) x0 H8))))) H6))))) (pr0_confluence t3 t5 H3
t2 H0)))))))))) t0 t1 H))).
x0)).(ex_intro2 T (\lambda (t: T).(pr1 t4 t)) (\lambda (t: T).(pr1 t5 t)) x0
H7 (pr1_t x t5 (pr1_pr0 t5 x H4) x0 H8))))) H6))))) (pr0_confluence t3 t5 H3
t2 H0)))))))))) t0 t1 H))).
t))) (\lambda (x0: T).(\lambda (H8: (pr1 t4 x0)).(\lambda (H9: (pr1 x
x0)).(ex_intro2 T (\lambda (t: T).(pr1 t4 t)) (\lambda (t: T).(pr1 t5 t)) x0
H8 (pr1_t x t5 H5 x0 H9))))) H7)))))) H4))))))))))) t0 t1 H))).
t))) (\lambda (x0: T).(\lambda (H8: (pr1 t4 x0)).(\lambda (H9: (pr1 x
x0)).(ex_intro2 T (\lambda (t: T).(pr1 t4 t)) (\lambda (t: T).(pr1 t5 t)) x0
H8 (pr1_t x t5 H5 x0 H9))))) H7)))))) H4))))))))))) t0 t1 H))).