(eq_ind_r T x2 (\lambda (t: T).(pr3 c x1 t)) H15 x0 H_y1) in (let H17 \def
(nf2_pr3_confluence c x H3 x0 H6 u1 H2) in (H8 (H17 (pr3_t x1 u1 c H11 x0
H16)) False))))))) H13)))))) H10))))) H7)))))) H4)))))) H1)))))))))))).
(eq_ind_r T x2 (\lambda (t: T).(pr3 c x1 t)) H15 x0 H_y1) in (let H17 \def
(nf2_pr3_confluence c x H3 x0 H6 u1 H2) in (H8 (H17 (pr3_t x1 u1 c H11 x0
H16)) False))))))) H13)))))) H10))))) H7)))))) H4)))))) H1)))))))))))).
(Bind Abst)) (H32 (pr3_t x3 u2 c H20 x5 H25)) (refl_equal T x6))) False))))
H29))))))))) H23)))))))) H18))))))) (pr3_confluence c u1 x1 H13 x H4)))))
H12)))))) H9)))))) H6)))))) H3)))))))))))).
(Bind Abst)) (H32 (pr3_t x3 u2 c H20 x5 H25)) (refl_equal T x6))) False))))
H29))))))))) H23)))))))) H18))))))) (pr3_confluence c u1 x1 H13 x H4)))))
H12)))))) H9)))))) H6)))))) H3)))))))))))).