DEFINITION iso_gen_sort()
TYPE =
       ∀u2:T.∀n1:nat.(iso (TSort n1) u2)→(ex nat λn2:nat.eq T u2 (TSort n2))
BODY =
Show proof