DEFINITION subst_sort()
TYPE =
       ∀v:T.∀d:nat.∀k:nat.(eq T (subst d v (TSort k)) (TSort k))
BODY =
Show proof