DEFINITION lift_sort()
TYPE =
       ∀n:nat.∀h:nat.∀d:nat.(eq T (lift h d (TSort n)) (TSort n))
BODY =
Show proof