DEFINITION lift_sort()
TYPE =
       ∀n:nat.∀h:nat.∀d:nat.(eq T (lift h d (TSort n)) (TSort n))
BODY =
        assume n: nat
        assume : nat
        assume : nat
          by (refl_equal . .)
          we proved eq T (TSort n) (TSort n)
          that is equivalent to eq T (lift __2 __1 (TSort n)) (TSort n)
       we proved ∀n:nat.nat→nat→(eq T (lift __2 __1 (TSort n)) (TSort n))