T).((eq T t (THead (Bind Abst) x0 t0)) \to (\forall (P: Prop).P)))) H10
(THead (Bind Abst) x5 x6) H24) in (let H28 \def (eq_ind T x (\lambda (t:
T).(nf2 c t)) H5 (THead (Bind Abst) x5 x6) H24) in (let H29 \def
T).((eq T t (THead (Bind Abst) x0 t0)) \to (\forall (P: Prop).P)))) H10
(THead (Bind Abst) x5 x6) H24) in (let H28 \def (eq_ind T x (\lambda (t:
T).(nf2 c t)) H5 (THead (Bind Abst) x5 x6) H24) in (let H29 \def
x5) x6) False (\lambda (H30: (nf2 c x5)).(\lambda (_: (nf2 (CHead c (Bind
Abst) x5) x6)).(let H32 \def (nf2_pr3_confluence c x0 H8 x5 H30 u2 H7) in
(H27 x6 (sym_eq T (THead (Bind Abst) x0 x6) (THead (Bind Abst) x5 x6)
x5) x6) False (\lambda (H30: (nf2 c x5)).(\lambda (_: (nf2 (CHead c (Bind
Abst) x5) x6)).(let H32 \def (nf2_pr3_confluence c x0 H8 x5 H30 u2 H7) in
(H27 x6 (sym_eq T (THead (Bind Abst) x0 x6) (THead (Bind Abst) x5 x6)