DEFINITION lift1_sort()
TYPE =
       ∀n:nat.∀is:PList.(eq T (lift1 is (TSort n)) (TSort n))
BODY =
Show proof