-t2)).(let TMP_1 \def (\lambda (t: T).(\lambda (t0: T).((nf2 c t) \to (eq T t
-t0)))) in (let TMP_4 \def (\lambda (t: T).(\lambda (H0: (nf2 c t)).(let TMP_2
-\def (pr0_refl t) in (let TMP_3 \def (pr2_free c t t TMP_2) in (H0 t
-TMP_3))))) in (let TMP_12 \def (\lambda (t0: T).(\lambda (t3: T).(\lambda
-(H0: (pr2 c t3 t0)).(\lambda (t4: T).(\lambda (_: (pr3 c t0 t4)).(\lambda
-(H2: (((nf2 c t0) \to (eq T t0 t4)))).(\lambda (H3: (nf2 c t3)).(let H4 \def
-H3 in (let TMP_5 \def (\lambda (t: T).(nf2 c t)) in (let TMP_6 \def (H4 t0
-H0) in (let H5 \def (eq_ind T t3 TMP_5 H3 t0 TMP_6) in (let TMP_7 \def
-(\lambda (t: T).(pr2 c t t0)) in (let TMP_8 \def (H4 t0 H0) in (let H6 \def
-(eq_ind T t3 TMP_7 H0 t0 TMP_8) in (let TMP_9 \def (\lambda (t: T).(eq T t
-t4)) in (let TMP_10 \def (H2 H5) in (let TMP_11 \def (H4 t0 H0) in (eq_ind_r
-T t0 TMP_9 TMP_10 t3 TMP_11)))))))))))))))))) in (pr3_ind c TMP_1 TMP_4
-TMP_12 t1 t2 H))))))).
+t2)).(pr3_ind c (\lambda (t: T).(\lambda (t0: T).((nf2 c t) \to (eq T t
+t0)))) (\lambda (t: T).(\lambda (H0: (nf2 c t)).(H0 t (pr2_free c t t
+(pr0_refl t))))) (\lambda (t0: T).(\lambda (t3: T).(\lambda (H0: (pr2 c t3
+t0)).(\lambda (t4: T).(\lambda (_: (pr3 c t0 t4)).(\lambda (H2: (((nf2 c t0)
+\to (eq T t0 t4)))).(\lambda (H3: (nf2 c t3)).(let H4 \def H3 in (let H5 \def
+(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)))).