-(THead (Bind Abst) u2 u)) \to (\forall (P: Prop).P))) (\lambda (u:
-T).(\lambda (H11: (pc3 c u1 (THead (Bind Abst) u2 u))).(\lambda (P:
-Prop).(let H12 \def H11 in (ex2_ind T (\lambda (t: T).(pr3 c u1 t)) (\lambda
-(t: T).(pr3 c (THead (Bind Abst) u2 u) t)) P (\lambda (x1: T).(\lambda (H13:
-(pr3 c u1 x1)).(\lambda (H14: (pr3 c (THead (Bind Abst) u2 u) x1)).(ex2_ind T
-(\lambda (t: T).(pr3 c x1 t)) (\lambda (t: T).(pr3 c x t)) P (\lambda (x2:
-T).(\lambda (H15: (pr3 c x1 x2)).(\lambda (H16: (pr3 c x x2)).(let H_y \def
-(nf2_pr3_unfold c x x2 H16 H5) in (let H17 \def (eq_ind_r T x2 (\lambda (t:
-T).(pr3 c x1 t)) H15 x H_y) in (let H18 \def (pr3_gen_abst c u2 u x1 H14) in
-(ex3_2_ind T T (\lambda (u3: T).(\lambda (t3: T).(eq T x1 (THead (Bind Abst)
-u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr3 c u2 u3))) (\lambda (_:
-T).(\lambda (t3: T).(\forall (b: B).(\forall (u0: T).(pr3 (CHead c (Bind b)
-u0) u t3))))) P (\lambda (x3: T).(\lambda (x4: T).(\lambda (H19: (eq T x1
-(THead (Bind Abst) x3 x4))).(\lambda (H20: (pr3 c u2 x3)).(\lambda (_:
-((\forall (b: B).(\forall (u0: T).(pr3 (CHead c (Bind b) u0) u x4))))).(let
-H22 \def (eq_ind T x1 (\lambda (t: T).(pr3 c t x)) H17 (THead (Bind Abst) x3
-x4) H19) in (let H23 \def (pr3_gen_abst c x3 x4 x H22) in (ex3_2_ind T T
-(\lambda (u3: T).(\lambda (t3: T).(eq T x (THead (Bind Abst) u3 t3))))
-(\lambda (u3: T).(\lambda (_: T).(pr3 c x3 u3))) (\lambda (_: T).(\lambda
-(t3: T).(\forall (b: B).(\forall (u0: T).(pr3 (CHead c (Bind b) u0) x4
-t3))))) P (\lambda (x5: T).(\lambda (x6: T).(\lambda (H24: (eq T x (THead
-(Bind Abst) x5 x6))).(\lambda (H25: (pr3 c x3 x5)).(\lambda (_: ((\forall (b:
-B).(\forall (u0: T).(pr3 (CHead c (Bind b) u0) x4 x6))))).(let H27 \def
-(eq_ind T x (\lambda (t: T).(\forall (t0: T).((eq T t (THead (Bind Abst) x0
-t0)) \to (\forall (P0: Prop).P0)))) 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 (nf2_gen_abst c x5 x6 H28) in (and_ind (nf2 c x5)
-(nf2 (CHead c (Bind Abst) x5) x6) P (\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) (f_equal3 K T T T THead (Bind Abst) (Bind Abst) x0 x5 x6 x6
-(refl_equal K (Bind Abst)) (H32 (pr3_t x3 u2 c H20 x5 H25)) (refl_equal T
-x6))) P)))) H29))))))))) H23)))))))) H18))))))) (pr3_confluence c u1 x1 H13 x
-H4))))) H12))))))) H9)))))) H6)))))) H3)))))))))))).
+(THead (Bind Abst) u2 u)) \to False)) (\lambda (u: T).(\lambda (H11: (pc3 c
+u1 (THead (Bind Abst) u2 u))).(let H12 \def H11 in (ex2_ind T (\lambda (t:
+T).(pr3 c u1 t)) (\lambda (t: T).(pr3 c (THead (Bind Abst) u2 u) t)) False
+(\lambda (x1: T).(\lambda (H13: (pr3 c u1 x1)).(\lambda (H14: (pr3 c (THead
+(Bind Abst) u2 u) x1)).(ex2_ind T (\lambda (t: T).(pr3 c x1 t)) (\lambda (t:
+T).(pr3 c x t)) False (\lambda (x2: T).(\lambda (H15: (pr3 c x1 x2)).(\lambda
+(H16: (pr3 c x x2)).(let H_y \def (nf2_pr3_unfold c x x2 H16 H5) in (let H17
+\def (eq_ind_r T x2 (\lambda (t: T).(pr3 c x1 t)) H15 x H_y) in (let H18 \def
+(pr3_gen_abst c u2 u x1 H14) in (ex3_2_ind T T (\lambda (u3: T).(\lambda (t3:
+T).(eq T x1 (THead (Bind Abst) u3 t3)))) (\lambda (u3: T).(\lambda (_:
+T).(pr3 c u2 u3))) (\lambda (_: T).(\lambda (t3: T).(\forall (b: B).(\forall
+(u0: T).(pr3 (CHead c (Bind b) u0) u t3))))) False (\lambda (x3: T).(\lambda
+(x4: T).(\lambda (H19: (eq T x1 (THead (Bind Abst) x3 x4))).(\lambda (H20:
+(pr3 c u2 x3)).(\lambda (_: ((\forall (b: B).(\forall (u0: T).(pr3 (CHead c
+(Bind b) u0) u x4))))).(let H22 \def (eq_ind T x1 (\lambda (t: T).(pr3 c t
+x)) H17 (THead (Bind Abst) x3 x4) H19) in (let H23 \def (pr3_gen_abst c x3 x4
+x H22) in (ex3_2_ind T T (\lambda (u3: T).(\lambda (t3: T).(eq T x (THead
+(Bind Abst) u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr3 c x3 u3)))
+(\lambda (_: T).(\lambda (t3: T).(\forall (b: B).(\forall (u0: T).(pr3 (CHead
+c (Bind b) u0) x4 t3))))) False (\lambda (x5: T).(\lambda (x6: T).(\lambda
+(H24: (eq T x (THead (Bind Abst) x5 x6))).(\lambda (H25: (pr3 c x3
+x5)).(\lambda (_: ((\forall (b: B).(\forall (u0: T).(pr3 (CHead c (Bind b)
+u0) x4 x6))))).(let H27 \def (eq_ind T x (\lambda (t: T).(\forall (t0:
+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
+(nf2_gen_abst c x5 x6 H28) in (and_ind (nf2 c x5) (nf2 (CHead c (Bind Abst)
+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)
+(f_equal3 K T T T THead (Bind Abst) (Bind Abst) x0 x5 x6 x6 (refl_equal K
+(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)))))))))))).