t1) H3) in (False_ind (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2
(THead (Bind Abst) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2)))
(\lambda (_: T).(\lambda (t3: T).(pr0 t1 t3)))) H4)))))))) y x H0))) H)))).
t1) H3) in (False_ind (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2
(THead (Bind Abst) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2)))
(\lambda (_: T).(\lambda (t3: T).(pr0 t1 t3)))) H4)))))))) y x H0))) H)))).