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