DEFINITION lift_gen_sort()
TYPE =
       ∀h:nat
         .∀d:nat
           .∀n:nat.∀t:T.(eq T (TSort n) (lift h d t))→(eq T t (TSort n))
BODY =
        assume h: nat
        assume d: nat
        assume n: nat
        assume t: T
          we proceed by induction on t to prove (eq T (TSort n) (lift h d t))→(eq T t (TSort n))
             case TSort : n0:nat ⇒
                the thesis becomes 
                ∀H:eq T (TSort n) (lift h d (TSort n0))
                  .eq T (TSort n0) (TSort n)
                   suppose H: eq T (TSort n) (lift h d (TSort n0))
                      consider H
                      we proved eq T (TSort n) (lift h d (TSort n0))
                      that is equivalent to eq T (TSort n) (TSort n0)
                      by (sym_eq . . . previous)
                      we proved eq T (TSort n0) (TSort n)

                      ∀H:eq T (TSort n) (lift h d (TSort n0))
                        .eq T (TSort n0) (TSort n)
             case TLRef : n0:nat ⇒
                the thesis becomes 
                ∀H:eq T (TSort n) (lift h d (TLRef n0))
                  .eq T (TLRef n0) (TSort n)
                   suppose H: eq T (TSort n) (lift h d (TLRef n0))
                      (h1) 
                         suppose : lt n0 d
                            (H1) 
                               (H1) 
                                  we proceed by induction on H to prove 
                                     <λ:T.Prop>
                                       CASE lift h d (TLRef n0) OF
                                         TSort ⇒True
                                       | TLRef ⇒False
                                       | THead   ⇒False
                                     case refl_equal : ⇒
                                        the thesis becomes 
                                        <λ:T.Prop>
                                          CASE TSort n OF
                                            TSort ⇒True
                                          | TLRef ⇒False
                                          | THead   ⇒False
                                           consider I
                                           we proved True

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

                                     <λ:T.Prop>
                                       CASE lift h d (TLRef n0) OF
                                         TSort ⇒True
                                       | TLRef ⇒False
                                       | THead   ⇒False
                               end of H1
                               consider H1
                               we proved 
                                  <λ:T.Prop>
                                    CASE lift h d (TLRef n0) OF
                                      TSort ⇒True
                                    | TLRef ⇒False
                                    | THead   ⇒False
                               that is equivalent to False
                               we proceed by induction on the previous result to prove lt n0 d
                               we proved lt n0 d
                               by (lift_lref_lt . . . previous)
                               we proved eq T (lift h d (TLRef n0)) (TLRef n0)
                               we proceed by induction on the previous result to prove eq T (TSort n) (TLRef n0)
                                  case refl_equal : ⇒
                                     the thesis becomes the hypothesis H
eq T (TSort n) (TLRef n0)
                            end of H1
                            (H2) 
                               we proceed by induction on H1 to prove 
                                  <λ:T.Prop>
                                    CASE TLRef n0 OF
                                      TSort ⇒True
                                    | TLRef ⇒False
                                    | THead   ⇒False
                                  case refl_equal : ⇒
                                     the thesis becomes 
                                     <λ:T.Prop>
                                       CASE TSort n OF
                                         TSort ⇒True
                                       | TLRef ⇒False
                                       | THead   ⇒False
                                        consider I
                                        we proved True

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

                                  <λ:T.Prop>
                                    CASE TLRef n0 OF
                                      TSort ⇒True
                                    | TLRef ⇒False
                                    | THead   ⇒False
                            end of H2
                            consider H2
                            we proved 
                               <λ:T.Prop>
                                 CASE TLRef n0 OF
                                   TSort ⇒True
                                 | TLRef ⇒False
                                 | THead   ⇒False
                            that is equivalent to False
                            we proceed by induction on the previous result to prove eq T (TLRef n0) (TSort n)
                            we proved eq T (TLRef n0) (TSort n)
(lt n0 d)→(eq T (TLRef n0) (TSort n))
                      end of h1
                      (h2) 
                         suppose : le d n0
                            (H1) 
                               (H1) 
                                  we proceed by induction on H to prove 
                                     <λ:T.Prop>
                                       CASE lift h d (TLRef n0) OF
                                         TSort ⇒True
                                       | TLRef ⇒False
                                       | THead   ⇒False
                                     case refl_equal : ⇒
                                        the thesis becomes 
                                        <λ:T.Prop>
                                          CASE TSort n OF
                                            TSort ⇒True
                                          | TLRef ⇒False
                                          | THead   ⇒False
                                           consider I
                                           we proved True

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

                                     <λ:T.Prop>
                                       CASE lift h d (TLRef n0) OF
                                         TSort ⇒True
                                       | TLRef ⇒False
                                       | THead   ⇒False
                               end of H1
                               consider H1
                               we proved 
                                  <λ:T.Prop>
                                    CASE lift h d (TLRef n0) OF
                                      TSort ⇒True
                                    | TLRef ⇒False
                                    | THead   ⇒False
                               that is equivalent to False
                               we proceed by induction on the previous result to prove le d n0
                               we proved le d n0
                               by (lift_lref_ge . . . previous)
                               we proved eq T (lift h d (TLRef n0)) (TLRef (plus n0 h))
                               we proceed by induction on the previous result to prove eq T (TSort n) (TLRef (plus n0 h))
                                  case refl_equal : ⇒
                                     the thesis becomes the hypothesis H
eq T (TSort n) (TLRef (plus n0 h))
                            end of H1
                            (H2) 
                               we proceed by induction on H1 to prove 
                                  <λ:T.Prop>
                                    CASE TLRef (plus n0 h) OF
                                      TSort ⇒True
                                    | TLRef ⇒False
                                    | THead   ⇒False
                                  case refl_equal : ⇒
                                     the thesis becomes 
                                     <λ:T.Prop>
                                       CASE TSort n OF
                                         TSort ⇒True
                                       | TLRef ⇒False
                                       | THead   ⇒False
                                        consider I
                                        we proved True

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

                                  <λ:T.Prop>
                                    CASE TLRef (plus n0 h) OF
                                      TSort ⇒True
                                    | TLRef ⇒False
                                    | THead   ⇒False
                            end of H2
                            consider H2
                            we proved 
                               <λ:T.Prop>
                                 CASE TLRef (plus n0 h) OF
                                   TSort ⇒True
                                 | TLRef ⇒False
                                 | THead   ⇒False
                            that is equivalent to False
                            we proceed by induction on the previous result to prove eq T (TLRef n0) (TSort n)
                            we proved eq T (TLRef n0) (TSort n)
(le d n0)→(eq T (TLRef n0) (TSort n))
                      end of h2
                      by (lt_le_e . . . h1 h2)
                      we proved eq T (TLRef n0) (TSort n)

                      ∀H:eq T (TSort n) (lift h d (TLRef n0))
                        .eq T (TLRef n0) (TSort n)
             case THead : k:K t0:T t1:T ⇒
                the thesis becomes 
                ∀H1:eq T (TSort n) (lift h d (THead k t0 t1))
                  .eq T (THead k t0 t1) (TSort n)
                () by induction hypothesis we know (eq T (TSort n) (lift h d t0))→(eq T t0 (TSort n))
                () by induction hypothesis we know (eq T (TSort n) (lift h d t1))→(eq T t1 (TSort n))
                   suppose H1: eq T (TSort n) (lift h d (THead k t0 t1))
                      (H2) 
                         by (lift_head . . . . .)
                         we proved 
                            eq
                              T
                              lift h d (THead k t0 t1)
                              THead k (lift h d t0) (lift h (s k d) t1)
                         we proceed by induction on the previous result to prove eq T (TSort n) (THead k (lift h d t0) (lift h (s k d) t1))
                            case refl_equal : ⇒
                               the thesis becomes the hypothesis H1
eq T (TSort n) (THead k (lift h d t0) (lift h (s k d) t1))
                      end of H2
                      (H3) 
                         we proceed by induction on H2 to prove 
                            <λ:T.Prop>
                              CASE THead k (lift h d t0) (lift h (s k d) t1) OF
                                TSort ⇒True
                              | TLRef ⇒False
                              | THead   ⇒False
                            case refl_equal : ⇒
                               the thesis becomes 
                               <λ:T.Prop>
                                 CASE TSort n OF
                                   TSort ⇒True
                                 | TLRef ⇒False
                                 | THead   ⇒False
                                  consider I
                                  we proved True

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

                            <λ:T.Prop>
                              CASE THead k (lift h d t0) (lift h (s k d) t1) OF
                                TSort ⇒True
                              | TLRef ⇒False
                              | THead   ⇒False
                      end of H3
                      consider H3
                      we proved 
                         <λ:T.Prop>
                           CASE THead k (lift h d t0) (lift h (s k d) t1) OF
                             TSort ⇒True
                           | TLRef ⇒False
                           | THead   ⇒False
                      that is equivalent to False
                      we proceed by induction on the previous result to prove eq T (THead k t0 t1) (TSort n)
                      we proved eq T (THead k t0 t1) (TSort n)

                      ∀H1:eq T (TSort n) (lift h d (THead k t0 t1))
                        .eq T (THead k t0 t1) (TSort n)
          we proved (eq T (TSort n) (lift h d t))→(eq T t (TSort n))
       we proved 
          ∀h:nat
            .∀d:nat
              .∀n:nat.∀t:T.(eq T (TSort n) (lift h d t))→(eq T t (TSort n))