DEFINITION subst1_gen_sort()
TYPE =
       ∀v:T.∀x:T.∀i:nat.∀n:nat.(subst1 i v (TSort n) x)→(eq T x (TSort n))
BODY =
Show proof