DEFINITION subst_sort()
TYPE =
       ∀v:T.∀d:nat.∀k:nat.(eq T (subst d v (TSort k)) (TSort k))
BODY =
        assume : T
        assume : nat
        assume k: nat
          by (refl_equal . .)
          we proved eq T (TSort k) (TSort k)
          that is equivalent to eq T (subst __2 __3 (TSort k)) (TSort k)
       we proved T→nat→∀k:nat.(eq T (subst __2 __3 (TSort k)) (TSort k))