DEFINITION subst0_gen_sort()
TYPE =
       ∀v:T.∀x:T.∀i:nat.∀n:nat.(subst0 i v (TSort n) x)→∀P:Prop.P
BODY =
Show proof