-(H3: (pr1 t3 t5)).(ex2_ind T (\lambda (t: T).(pr1 t5 t)) (\lambda (t: T).(pr1
-t2 t)) (ex2 T (\lambda (t: T).(pr1 t4 t)) (\lambda (t: T).(pr1 t5 t)))
-(\lambda (x: T).(\lambda (H4: (pr1 t5 x)).(\lambda (H5: (pr1 t2 x)).(ex2_ind
-T (\lambda (t: T).(pr1 t4 t)) (\lambda (t: T).(pr1 x t)) (ex2 T (\lambda (t:
-T).(pr1 t4 t)) (\lambda (t: T).(pr1 t5 t))) (\lambda (x0: T).(\lambda (H6:
-(pr1 t4 x0)).(\lambda (H7: (pr1 x x0)).(ex_intro2 T (\lambda (t: T).(pr1 t4
-t)) (\lambda (t: T).(pr1 t5 t)) x0 H6 (pr1_t x t5 H4 x0 H7))))) (H2 x H5)))))
-(pr1_strip t3 t5 H3 t2 H0)))))))))) t0 t1 H))).
+(H3: (pr1 t3 t5)).(let H_x \def (pr1_strip t3 t5 H3 t2 H0) in (let H4 \def
+H_x in (ex2_ind T (\lambda (t: T).(pr1 t5 t)) (\lambda (t: T).(pr1 t2 t))
+(ex2 T (\lambda (t: T).(pr1 t4 t)) (\lambda (t: T).(pr1 t5 t))) (\lambda (x:
+T).(\lambda (H5: (pr1 t5 x)).(\lambda (H6: (pr1 t2 x)).(let H_x0 \def (H2 x
+H6) in (let H7 \def H_x0 in (ex2_ind T (\lambda (t: T).(pr1 t4 t)) (\lambda
+(t: T).(pr1 x t)) (ex2 T (\lambda (t: T).(pr1 t4 t)) (\lambda (t: T).(pr1 t5
+t))) (\lambda (x0: T).(\lambda (H8: (pr1 t4 x0)).(\lambda (H9: (pr1 x
+x0)).(ex_intro2 T (\lambda (t: T).(pr1 t4 t)) (\lambda (t: T).(pr1 t5 t)) x0
+H8 (pr1_t x t5 H5 x0 H9))))) H7)))))) H4))))))))))) t0 t1 H))).