T).(\lambda (_: (ty3 g c t4 t0)).(\lambda (H3: ((\forall (c2: C).((wf3 g c
c2) \to (ty3 g c2 t4 t0))))).(\lambda (c2: C).(\lambda (H4: (wf3 g c
c2)).(ty3_cast g c2 t3 t4 (H1 c2 H4) t0 (H3 c2 H4)))))))))))) c1 t1 t2 H))))).
T).(\lambda (_: (ty3 g c t4 t0)).(\lambda (H3: ((\forall (c2: C).((wf3 g c
c2) \to (ty3 g c2 t4 t0))))).(\lambda (c2: C).(\lambda (H4: (wf3 g c
c2)).(ty3_cast g c2 t3 t4 (H1 c2 H4) t0 (H3 c2 H4)))))))))))) c1 t1 t2 H))))).