x)).(\lambda (H2: (pr1 t2 x)).(ex_intro2 T (\lambda (t: T).(pr3 c t1 t))
(\lambda (t: T).(pr3 c t2 t)) x (pr3_pr1 t1 x H1 c) (pr3_pr1 t2 x H2 c)))))
H0))))).
x)).(\lambda (H2: (pr1 t2 x)).(ex_intro2 T (\lambda (t: T).(pr3 c t1 t))
(\lambda (t: T).(pr3 c t2 t)) x (pr3_pr1 t1 x H1 c) (pr3_pr1 t2 x H2 c)))))
H0))))).