-T).(\lambda (H0: (pc1 t2 t3)).(let H1 \def H0 in (let TMP_1 \def (\lambda (t:
-T).(pr1 t2 t)) in (let TMP_2 \def (\lambda (t: T).(pr1 t3 t)) in (let TMP_3
-\def (pc1 t1 t3) in (let TMP_17 \def (\lambda (x: T).(\lambda (H2: (pr1 t2
-x)).(\lambda (H3: (pr1 t3 x)).(let H4 \def H in (let TMP_4 \def (\lambda (t:
-T).(pr1 t1 t)) in (let TMP_5 \def (\lambda (t: T).(pr1 t2 t)) in (let TMP_6
-\def (pc1 t1 t3) in (let TMP_16 \def (\lambda (x0: T).(\lambda (H5: (pr1 t1
-x0)).(\lambda (H6: (pr1 t2 x0)).(let TMP_7 \def (\lambda (t: T).(pr1 x0 t))
-in (let TMP_8 \def (\lambda (t: T).(pr1 x t)) in (let TMP_9 \def (pc1 t1 t3)
-in (let TMP_14 \def (\lambda (x1: T).(\lambda (H7: (pr1 x0 x1)).(\lambda (H8:
-(pr1 x x1)).(let TMP_10 \def (\lambda (t: T).(pr1 t1 t)) in (let TMP_11 \def
-(\lambda (t: T).(pr1 t3 t)) in (let TMP_12 \def (pr1_t x0 t1 H5 x1 H7) in
-(let TMP_13 \def (pr1_t x t3 H3 x1 H8) in (ex_intro2 T TMP_10 TMP_11 x1
-TMP_12 TMP_13)))))))) in (let TMP_15 \def (pr1_confluence t2 x0 H6 x H2) in
-(ex2_ind T TMP_7 TMP_8 TMP_9 TMP_14 TMP_15))))))))) in (ex2_ind T TMP_4 TMP_5
-TMP_6 TMP_16 H4))))))))) in (ex2_ind T TMP_1 TMP_2 TMP_3 TMP_17 H1)))))))))).
+T).(\lambda (H0: (pc1 t2 t3)).(let H1 \def H0 in (ex2_ind T (\lambda (t:
+T).(pr1 t2 t)) (\lambda (t: T).(pr1 t3 t)) (pc1 t1 t3) (\lambda (x:
+T).(\lambda (H2: (pr1 t2 x)).(\lambda (H3: (pr1 t3 x)).(let H4 \def H in
+(ex2_ind T (\lambda (t: T).(pr1 t1 t)) (\lambda (t: T).(pr1 t2 t)) (pc1 t1
+t3) (\lambda (x0: T).(\lambda (H5: (pr1 t1 x0)).(\lambda (H6: (pr1 t2
+x0)).(ex2_ind T (\lambda (t: T).(pr1 x0 t)) (\lambda (t: T).(pr1 x t)) (pc1
+t1 t3) (\lambda (x1: T).(\lambda (H7: (pr1 x0 x1)).(\lambda (H8: (pr1 x
+x1)).(ex_intro2 T (\lambda (t: T).(pr1 t1 t)) (\lambda (t: T).(pr1 t3 t)) x1
+(pr1_t x0 t1 H5 x1 H7) (pr1_t x t3 H3 x1 H8))))) (pr1_confluence t2 x0 H6 x
+H2))))) H4))))) H1)))))).