c4 H1 (TSort O) (TSort (next g O)) (ty3_sort g c4 O) Void)))))))) (\lambda
(c3: C).(\lambda (c4: C).(\lambda (_: (wf3 g c3 c4)).(\lambda (H1: (wf3 g c4
c4)).(\lambda (_: T).(\lambda (_: F).H1)))))) c1 c2 H)))).
c4 H1 (TSort O) (TSort (next g O)) (ty3_sort g c4 O) Void)))))))) (\lambda
(c3: C).(\lambda (c4: C).(\lambda (_: (wf3 g c3 c4)).(\lambda (H1: (wf3 g c4
c4)).(\lambda (_: T).(\lambda (_: F).H1)))))) c1 c2 H)))).