T).(\lambda (H1: (pr1 t1 x)).(\lambda (H2: (pr1 t2 x)).(ex_intro2 T (\lambda
(t: T).(pr1 (THead k u t1) t)) (\lambda (t: T).(pr1 (THead k u t2) t)) (THead
k u x) (pr1_head_2 t1 x H1 u k) (pr1_head_2 t2 x H2 u k))))) H0)))))).
T).(\lambda (H1: (pr1 t1 x)).(\lambda (H2: (pr1 t2 x)).(ex_intro2 T (\lambda
(t: T).(pr1 (THead k u t1) t)) (\lambda (t: T).(pr1 (THead k u t2) t)) (THead
k u x) (pr1_head_2 t1 x H1 u k) (pr1_head_2 t2 x H2 u k))))) H0)))))).