T).(ty3 g c2 x0 t4)) False (\lambda (x: T).(\lambda (_: (ty3 g c2 x0 x)).(H5
x0 H9))) (ty3_correct g c2 t x0 H9)))))) (ty3_gen_cast g c2 t0 t t3 H6))))))
H4))) f H2))) k H1))))))) t2))) c t1))).
T).(ty3 g c2 x0 t4)) False (\lambda (x: T).(\lambda (_: (ty3 g c2 x0 x)).(H5
x0 H9))) (ty3_correct g c2 t x0 H9)))))) (ty3_gen_cast g c2 t0 t t3 H6))))))
H4))) f H2))) k H1))))))) t2))) c t1))).