DEFINITION subst0_gen_sort()
TYPE =
       ∀v:T.∀x:T.∀i:nat.∀n:nat.(subst0 i v (TSort n) x)→∀P:Prop.P
BODY =
        assume v: T
        assume x: T
        assume i: nat
        assume n: nat
        suppose H: subst0 i v (TSort n) x
        assume P: Prop
           assume y: T
           suppose H0: subst0 i v y x
             we proceed by induction on H0 to prove (eq T y (TSort n))→P
                case subst0_lref : :T i0:nat ⇒
                   the thesis becomes ∀H1:(eq T (TLRef i0) (TSort n)).P
                      suppose H1: eq T (TLRef i0) (TSort n)
                         (H2) 
                            we proceed by induction on H1 to prove 
                               <λ:T.Prop>
                                 CASE TSort n OF
                                   TSort ⇒False
                                 | TLRef ⇒True
                                 | THead   ⇒False
                               case refl_equal : ⇒
                                  the thesis becomes 
                                  <λ:T.Prop>
                                    CASE TLRef i0 OF
                                      TSort ⇒False
                                    | TLRef ⇒True
                                    | THead   ⇒False
                                     consider I
                                     we proved True

                                        <λ:T.Prop>
                                          CASE TLRef i0 OF
                                            TSort ⇒False
                                          | TLRef ⇒True
                                          | THead   ⇒False

                               <λ:T.Prop>
                                 CASE TSort n OF
                                   TSort ⇒False
                                 | TLRef ⇒True
                                 | THead   ⇒False
                         end of H2
                         consider H2
                         we proved 
                            <λ:T.Prop>
                              CASE TSort n OF
                                TSort ⇒False
                              | TLRef ⇒True
                              | THead   ⇒False
                         that is equivalent to False
                         we proceed by induction on the previous result to prove P
                         we proved P
∀H1:(eq T (TLRef i0) (TSort n)).P
                case subst0_fst : v0:T u2:T u1:T i0:nat :subst0 i0 v0 u1 u2 t:T k:K ⇒
                   the thesis becomes ∀H3:(eq T (THead k u1 t) (TSort n)).P
                   () by induction hypothesis we know (eq T u1 (TSort n))→P
                      suppose H3: eq T (THead k u1 t) (TSort n)
                         (H4) 
                            we proceed by induction on H3 to prove 
                               <λ:T.Prop>
                                 CASE TSort n OF
                                   TSort ⇒False
                                 | TLRef ⇒False
                                 | THead   ⇒True
                               case refl_equal : ⇒
                                  the thesis becomes 
                                  <λ:T.Prop>
                                    CASE THead k u1 t OF
                                      TSort ⇒False
                                    | TLRef ⇒False
                                    | THead   ⇒True
                                     consider I
                                     we proved True

                                        <λ:T.Prop>
                                          CASE THead k u1 t OF
                                            TSort ⇒False
                                          | TLRef ⇒False
                                          | THead   ⇒True

                               <λ:T.Prop>
                                 CASE TSort n OF
                                   TSort ⇒False
                                 | TLRef ⇒False
                                 | THead   ⇒True
                         end of H4
                         consider H4
                         we proved 
                            <λ:T.Prop>
                              CASE TSort n OF
                                TSort ⇒False
                              | TLRef ⇒False
                              | THead   ⇒True
                         that is equivalent to False
                         we proceed by induction on the previous result to prove P
                         we proved P
∀H3:(eq T (THead k u1 t) (TSort n)).P
                case subst0_snd : k:K v0:T t2:T t1:T i0:nat :subst0 (s k i0) v0 t1 t2 u:T ⇒
                   the thesis becomes ∀H3:(eq T (THead k u t1) (TSort n)).P
                   () by induction hypothesis we know (eq T t1 (TSort n))→P
                      suppose H3: eq T (THead k u t1) (TSort n)
                         (H4) 
                            we proceed by induction on H3 to prove 
                               <λ:T.Prop>
                                 CASE TSort n OF
                                   TSort ⇒False
                                 | TLRef ⇒False
                                 | THead   ⇒True
                               case refl_equal : ⇒
                                  the thesis becomes 
                                  <λ:T.Prop>
                                    CASE THead k u t1 OF
                                      TSort ⇒False
                                    | TLRef ⇒False
                                    | THead   ⇒True
                                     consider I
                                     we proved True

                                        <λ:T.Prop>
                                          CASE THead k u t1 OF
                                            TSort ⇒False
                                          | TLRef ⇒False
                                          | THead   ⇒True

                               <λ:T.Prop>
                                 CASE TSort n OF
                                   TSort ⇒False
                                 | TLRef ⇒False
                                 | THead   ⇒True
                         end of H4
                         consider H4
                         we proved 
                            <λ:T.Prop>
                              CASE TSort n OF
                                TSort ⇒False
                              | TLRef ⇒False
                              | THead   ⇒True
                         that is equivalent to False
                         we proceed by induction on the previous result to prove P
                         we proved P
∀H3:(eq T (THead k u t1) (TSort n)).P
                case subst0_both : v0:T u1:T u2:T i0:nat :subst0 i0 v0 u1 u2 k:K t1:T t2:T :subst0 (s k i0) v0 t1 t2 ⇒
                   the thesis becomes ∀H5:(eq T (THead k u1 t1) (TSort n)).P
                   () by induction hypothesis we know (eq T u1 (TSort n))→P
                   () by induction hypothesis we know (eq T t1 (TSort n))→P
                      suppose H5: eq T (THead k u1 t1) (TSort n)
                         (H6) 
                            we proceed by induction on H5 to prove 
                               <λ:T.Prop>
                                 CASE TSort n OF
                                   TSort ⇒False
                                 | TLRef ⇒False
                                 | THead   ⇒True
                               case refl_equal : ⇒
                                  the thesis becomes 
                                  <λ:T.Prop>
                                    CASE THead k u1 t1 OF
                                      TSort ⇒False
                                    | TLRef ⇒False
                                    | THead   ⇒True
                                     consider I
                                     we proved True

                                        <λ:T.Prop>
                                          CASE THead k u1 t1 OF
                                            TSort ⇒False
                                          | TLRef ⇒False
                                          | THead   ⇒True

                               <λ:T.Prop>
                                 CASE TSort n OF
                                   TSort ⇒False
                                 | TLRef ⇒False
                                 | THead   ⇒True
                         end of H6
                         consider H6
                         we proved 
                            <λ:T.Prop>
                              CASE TSort n OF
                                TSort ⇒False
                              | TLRef ⇒False
                              | THead   ⇒True
                         that is equivalent to False
                         we proceed by induction on the previous result to prove P
                         we proved P
∀H5:(eq T (THead k u1 t1) (TSort n)).P
             we proved (eq T y (TSort n))→P
          we proved ∀y:T.(subst0 i v y x)→(eq T y (TSort n))→P
          by (insert_eq . . . . previous H)
          we proved P
       we proved ∀v:T.∀x:T.∀i:nat.∀n:nat.(subst0 i v (TSort n) x)→∀P:Prop.P