Cast) t4 t3) t))) (\lambda (x: T).(\lambda (H5: (ty3 g c0 t4 x)).(ex_intro T
(\lambda (t: T).(ty3 g c0 (THead (Flat Cast) t4 t3) t)) (THead (Flat Cast) x
t4) (ty3_cast g c0 t3 t4 H2 x H5)))) H4)))))))))) c t1 t2 H))))).
Cast) t4 t3) t))) (\lambda (x: T).(\lambda (H5: (ty3 g c0 t4 x)).(ex_intro T
(\lambda (t: T).(ty3 g c0 (THead (Flat Cast) t4 t3) t)) (THead (Flat Cast) x
t4) (ty3_cast g c0 t3 t4 H2 x H5)))) H4)))))))))) c t1 t2 H))))).