in (let H3 \def (eq_ind_r T t2 (\lambda (t0: T).((eq T t t0) \to (\forall (P:
Prop).P))) H0 t H_y) in (eq_ind T t (\lambda (t0: T).(sn3 c t0)) (H3
(refl_equal T t) (sn3 c t)) t2 H_y)))))))))).
in (let H3 \def (eq_ind_r T t2 (\lambda (t0: T).((eq T t t0) \to (\forall (P:
Prop).P))) H0 t H_y) in (eq_ind T t (\lambda (t0: T).(sn3 c t0)) (H3
(refl_equal T t) (sn3 c t)) t2 H_y)))))))))).