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 =
        assume v: T
        assume x: T
        assume i: nat
        assume n: nat
        suppose H: subst1 i v (TSort n) x
          we proceed by induction on H to prove eq T x (TSort n)
             case subst1_refl : ⇒
                the thesis becomes eq T (TSort n) (TSort n)
                   by (refl_equal . .)
eq T (TSort n) (TSort n)
             case subst1_single : t2:T H0:subst0 i v (TSort n) t2 ⇒
                the thesis becomes eq T t2 (TSort n)
                   by (subst0_gen_sort . . . . H0 .)
eq T t2 (TSort n)
          we proved eq T x (TSort n)
       we proved ∀v:T.∀x:T.∀i:nat.∀n:nat.(subst1 i v (TSort n) x)→(eq T x (TSort n))