t2)).(sty0_correct g c t1 t2 H0))) (\lambda (t0: T).(\lambda (_: (sty1 g c t1
t0)).(\lambda (_: (ex T (\lambda (t2: T).(sty0 g c t0 t2)))).(\lambda (t2:
T).(\lambda (H2: (sty0 g c t0 t2)).(sty0_correct g c t0 t2 H2)))))) t H))))).
t2)).(sty0_correct g c t1 t2 H0))) (\lambda (t0: T).(\lambda (_: (sty1 g c t1
t0)).(\lambda (_: (ex T (\lambda (t2: T).(sty0 g c t0 t2)))).(\lambda (t2:
T).(\lambda (H2: (sty0 g c t0 t2)).(sty0_correct g c t0 t2 H2)))))) t H))))).