(eq_ind T t3 (\lambda (t: T).(nf2 c t)) H3 t0 (H4 t0 H0)) in (let H6 \def
(eq_ind T t3 (\lambda (t: T).(pr2 c t t0)) H0 t0 (H4 t0 H0)) in (eq_ind_r T
t0 (\lambda (t: T).(eq T t t4)) (H2 H5) t3 (H4 t0 H0)))))))))))) t1 t2 H)))).
(eq_ind T t3 (\lambda (t: T).(nf2 c t)) H3 t0 (H4 t0 H0)) in (let H6 \def
(eq_ind T t3 (\lambda (t: T).(pr2 c t t0)) H0 t0 (H4 t0 H0)) in (eq_ind_r T
t0 (\lambda (t: T).(eq T t t4)) (H2 H5) t3 (H4 t0 H0)))))))))))) t1 t2 H)))).