DEFINITION subst1_lift_S()
TYPE =
       ∀u:T
         .∀i:nat
           .∀h:nat
             .le h i
               →subst1 i (TLRef h) (lift (S h) (S i) u) (lift (S h) i u)
BODY =
       assume u: T
          we proceed by induction on u to prove 
             ∀i:nat
               .∀h:nat
                 .le h i
                   →subst1 i (TLRef h) (lift (S h) (S i) u) (lift (S h) i u)
             case TSort : n:nat ⇒
                the thesis becomes 
                ∀i:nat
                  .∀h:nat
                    .le h i
                      →(subst1
                           i
                           TLRef h
                           lift (S h) (S i) (TSort n)
                           lift (S h) i (TSort n))
                    assume i: nat
                    assume h: nat
                    suppose : le h i
                      (h1) 
                         (h1) 
                            by (subst1_refl . . .)
subst1 i (TLRef h) (TSort n) (TSort n)
                         end of h1
                         (h2) 
                            by (lift_sort . . .)
eq T (lift (S h) i (TSort n)) (TSort n)
                         end of h2
                         by (eq_ind_r . . . h1 . h2)
subst1 i (TLRef h) (TSort n) (lift (S h) i (TSort n))
                      end of h1
                      (h2) 
                         by (lift_sort . . .)
eq T (lift (S h) (S i) (TSort n)) (TSort n)
                      end of h2
                      by (eq_ind_r . . . h1 . h2)
                      we proved 
                         subst1
                           i
                           TLRef h
                           lift (S h) (S i) (TSort n)
                           lift (S h) i (TSort n)

                      ∀i:nat
                        .∀h:nat
                          .le h i
                            →(subst1
                                 i
                                 TLRef h
                                 lift (S h) (S i) (TSort n)
                                 lift (S h) i (TSort n))
             case TLRef : n:nat ⇒
                the thesis becomes 
                ∀i:nat
                  .∀h:nat
                    .∀H:le h i
                      .subst1
                        i
                        TLRef h
                        lift (S h) (S i) (TLRef n)
                        lift (S h) i (TLRef n)
                    assume i: nat
                    assume h: nat
                    suppose H: le h i
                      (h1) 
                         suppose H0: lt n i
                            (h1) 
                               (h1) 
                                  by (subst1_refl . . .)
subst1 i (TLRef h) (TLRef n) (TLRef n)
                               end of h1
                               (h2) 
                                  by (lift_lref_lt . . . H0)
eq T (lift (S h) i (TLRef n)) (TLRef n)
                               end of h2
                               by (eq_ind_r . . . h1 . h2)
subst1 i (TLRef h) (TLRef n) (lift (S h) i (TLRef n))
                            end of h1
                            (h2) 
                               consider H0
                               we proved lt n i
                               that is equivalent to le (S n) i
                               by (le_S . . previous)
                               we proved le (S n) (S i)
                               that is equivalent to lt n (S i)
                               by (lift_lref_lt . . . previous)
eq T (lift (S h) (S i) (TLRef n)) (TLRef n)
                            end of h2
                            by (eq_ind_r . . . h1 . h2)
                            we proved 
                               subst1
                                 i
                                 TLRef h
                                 lift (S h) (S i) (TLRef n)
                                 lift (S h) i (TLRef n)

                            lt n i
                              →(subst1
                                   i
                                   TLRef h
                                   lift (S h) (S i) (TLRef n)
                                   lift (S h) i (TLRef n))
                      end of h1
                      (h2) 
                         suppose H0: eq nat n i
                            we proceed by induction on H0 to prove 
                               subst1
                                 i
                                 TLRef h
                                 lift (S h) (S i) (TLRef n)
                                 lift (S h) i (TLRef n)
                               case refl_equal : ⇒
                                  the thesis becomes 
                                  subst1
                                    n
                                    TLRef h
                                    lift (S h) (S n) (TLRef n)
                                    lift (S h) n (TLRef n)
                                     (h1) 
                                        (h1) 
                                           by (plus_n_Sm . .)
                                           we proved eq nat (S (plus n h)) (plus n (S h))
                                           we proceed by induction on the previous result to prove subst1 n (TLRef h) (TLRef n) (TLRef (plus n (S h)))
                                              case refl_equal : ⇒
                                                 the thesis becomes subst1 n (TLRef h) (TLRef n) (TLRef (S (plus n h)))
                                                    (h1) 
                                                       by (plus_n_Sm . .)
                                                       we proved eq nat (S (plus h n)) (plus h (S n))
                                                       by (sym_eq . . . previous)
                                                       we proved eq nat (plus h (S n)) (S (plus h n))
                                                       we proceed by induction on the previous result to prove subst1 n (TLRef h) (TLRef n) (TLRef (S (plus h n)))
                                                          case refl_equal : ⇒
                                                             the thesis becomes subst1 n (TLRef h) (TLRef n) (TLRef (plus h (S n)))
                                                                by (le_O_n .)
                                                                we proved le O h
                                                                by (lift_lref_ge . . . previous)
                                                                we proved eq T (lift (S n) O (TLRef h)) (TLRef (plus h (S n)))
                                                                we proceed by induction on the previous result to prove subst1 n (TLRef h) (TLRef n) (TLRef (plus h (S n)))
                                                                   case refl_equal : ⇒
                                                                      the thesis becomes subst1 n (TLRef h) (TLRef n) (lift (S n) O (TLRef h))
                                                                         by (subst0_lref . .)
                                                                         we proved subst0 n (TLRef h) (TLRef n) (lift (S n) O (TLRef h))
                                                                         by (subst1_single . . . . previous)
subst1 n (TLRef h) (TLRef n) (lift (S n) O (TLRef h))
subst1 n (TLRef h) (TLRef n) (TLRef (plus h (S n)))
subst1 n (TLRef h) (TLRef n) (TLRef (S (plus h n)))
                                                    end of h1
                                                    (h2) 
                                                       by (plus_sym . .)
eq nat (plus n h) (plus h n)
                                                    end of h2
                                                    by (eq_ind_r . . . h1 . h2)
subst1 n (TLRef h) (TLRef n) (TLRef (S (plus n h)))
subst1 n (TLRef h) (TLRef n) (TLRef (plus n (S h)))
                                        end of h1
                                        (h2) 
                                           by (le_n .)
                                           we proved le n n
                                           by (lift_lref_ge . . . previous)
eq T (lift (S h) n (TLRef n)) (TLRef (plus n (S h)))
                                        end of h2
                                        by (eq_ind_r . . . h1 . h2)
subst1 n (TLRef h) (TLRef n) (lift (S h) n (TLRef n))
                                     end of h1
                                     (h2) 
                                        by (le_n .)
                                        we proved le (S n) (S n)
                                        that is equivalent to lt n (S n)
                                        by (lift_lref_lt . . . previous)
eq T (lift (S h) (S n) (TLRef n)) (TLRef n)
                                     end of h2
                                     by (eq_ind_r . . . h1 . h2)

                                        subst1
                                          n
                                          TLRef h
                                          lift (S h) (S n) (TLRef n)
                                          lift (S h) n (TLRef n)
                            we proved 
                               subst1
                                 i
                                 TLRef h
                                 lift (S h) (S i) (TLRef n)
                                 lift (S h) i (TLRef n)

                            eq nat n i
                              →(subst1
                                   i
                                   TLRef h
                                   lift (S h) (S i) (TLRef n)
                                   lift (S h) i (TLRef n))
                      end of h2
                      (h3) 
                         suppose H0: lt i n
                            (h1) 
                               (h1) 
                                  by (subst1_refl . . .)

                                     subst1 i (TLRef h) (TLRef (plus n (S h))) (TLRef (plus n (S h)))
                               end of h1
                               (h2) 
                                  consider H0
                                  we proved lt i n
                                  that is equivalent to le (S i) n
                                  by (le_S . . previous)
                                  we proved le (S i) (S n)
                                  by (le_S_n . . previous)
                                  we proved le i n
                                  by (lift_lref_ge . . . previous)
eq T (lift (S h) i (TLRef n)) (TLRef (plus n (S h)))
                               end of h2
                               by (eq_ind_r . . . h1 . h2)

                                  subst1
                                    i
                                    TLRef h
                                    TLRef (plus n (S h))
                                    lift (S h) i (TLRef n)
                            end of h1
                            (h2) 
                               consider H0
                               we proved lt i n
                               that is equivalent to le (S i) n
                               by (lift_lref_ge . . . previous)
eq T (lift (S h) (S i) (TLRef n)) (TLRef (plus n (S h)))
                            end of h2
                            by (eq_ind_r . . . h1 . h2)
                            we proved 
                               subst1
                                 i
                                 TLRef h
                                 lift (S h) (S i) (TLRef n)
                                 lift (S h) i (TLRef n)

                            lt i n
                              →(subst1
                                   i
                                   TLRef h
                                   lift (S h) (S i) (TLRef n)
                                   lift (S h) i (TLRef n))
                      end of h3
                      by (lt_eq_gt_e . . . h1 h2 h3)
                      we proved 
                         subst1
                           i
                           TLRef h
                           lift (S h) (S i) (TLRef n)
                           lift (S h) i (TLRef n)

                      ∀i:nat
                        .∀h:nat
                          .∀H:le h i
                            .subst1
                              i
                              TLRef h
                              lift (S h) (S i) (TLRef n)
                              lift (S h) i (TLRef n)
             case THead : k:K t:T t0:T ⇒
                the thesis becomes 
                ∀i:nat
                  .∀h:nat
                    .∀H1:le h i
                      .subst1
                        i
                        TLRef h
                        lift (S h) (S i) (THead k t t0)
                        lift (S h) i (THead k t t0)
                (H) by induction hypothesis we know 
                   ∀i:nat
                     .∀h:nat
                       .le h i
                         →subst1 i (TLRef h) (lift (S h) (S i) t) (lift (S h) i t)
                (H0) by induction hypothesis we know 
                   ∀i:nat
                     .∀h:nat
                       .(le h i)→(subst1 i (TLRef h) (lift (S h) (S i) t0) (lift (S h) i t0))
                    assume i: nat
                    assume h: nat
                    suppose H1: le h i
                      (h1) 
                         (h1) 
                            (h1) 
                               by (H . . H1)
subst1 i (TLRef h) (lift (S h) (S i) t) (lift (S h) i t)
                            end of h1
                            (h2) 
                               (h1) 
                                  by (s_inc . .)
                                  we proved le i (s k i)
                                  by (le_trans . . . H1 previous)
                                  we proved le h (s k i)
                                  by (H0 . . previous)

                                     subst1
                                       s k i
                                       TLRef h
                                       lift (S h) (S (s k i)) t0
                                       lift (S h) (s k i) t0
                               end of h1
                               (h2) 
                                  by (s_S . .)
eq nat (s k (S i)) (S (s k i))
                               end of h2
                               by (eq_ind_r . . . h1 . h2)

                                  subst1
                                    s k i
                                    TLRef h
                                    lift (S h) (s k (S i)) t0
                                    lift (S h) (s k i) t0
                            end of h2
                            by (subst1_head . . . . h1 . . . h2)

                               subst1
                                 i
                                 TLRef h
                                 THead k (lift (S h) (S i) t) (lift (S h) (s k (S i)) t0)
                                 THead k (lift (S h) i t) (lift (S h) (s k i) t0)
                         end of h1
                         (h2) 
                            by (lift_head . . . . .)

                               eq
                                 T
                                 lift (S h) i (THead k t t0)
                                 THead k (lift (S h) i t) (lift (S h) (s k i) t0)
                         end of h2
                         by (eq_ind_r . . . h1 . h2)

                            subst1
                              i
                              TLRef h
                              THead k (lift (S h) (S i) t) (lift (S h) (s k (S i)) t0)
                              lift (S h) i (THead k t t0)
                      end of h1
                      (h2) 
                         by (lift_head . . . . .)

                            eq
                              T
                              lift (S h) (S i) (THead k t t0)
                              THead k (lift (S h) (S i) t) (lift (S h) (s k (S i)) t0)
                      end of h2
                      by (eq_ind_r . . . h1 . h2)
                      we proved 
                         subst1
                           i
                           TLRef h
                           lift (S h) (S i) (THead k t t0)
                           lift (S h) i (THead k t t0)

                      ∀i:nat
                        .∀h:nat
                          .∀H1:le h i
                            .subst1
                              i
                              TLRef h
                              lift (S h) (S i) (THead k t t0)
                              lift (S h) i (THead k t t0)
          we proved 
             ∀i:nat
               .∀h:nat
                 .le h i
                   →subst1 i (TLRef h) (lift (S h) (S i) u) (lift (S h) i u)
       we proved 
          ∀u:T
            .∀i:nat
              .∀h:nat
                .le h i
                  →subst1 i (TLRef h) (lift (S h) (S i) u) (lift (S h) i u)