DEFINITION lifts_tapp()
TYPE =
       ∀h:nat
         .∀d:nat
           .∀v:T
             .∀vs:TList
               .eq
                 TList
                 lifts h d (TApp vs v)
                 TApp (lifts h d vs) (lift h d v)
BODY =
        assume h: nat
        assume d: nat
        assume v: T
        assume vs: TList
          we proceed by induction on vs to prove 
             eq
               TList
               lifts h d (TApp vs v)
               TApp (lifts h d vs) (lift h d v)
             case TNil : ⇒
                the thesis becomes 
                eq
                  TList
                  lifts h d (TApp TNil v)
                  TApp (lifts h d TNil) (lift h d v)
                   by (refl_equal . .)
                   we proved eq TList (TCons (lift h d v) TNil) (TCons (lift h d v) TNil)

                      eq
                        TList
                        lifts h d (TApp TNil v)
                        TApp (lifts h d TNil) (lift h d v)
             case TCons : t:T t0:TList ⇒
                the thesis becomes 
                eq
                  TList
                  lifts h d (TApp (TCons t t0) v)
                  TApp (lifts h d (TCons t t0)) (lift h d v)
                (H) by induction hypothesis we know 
                   eq TList (lifts h d (TApp t0 v)) (TApp (lifts h d t0) (lift h d v))
                   by (refl_equal . .)
                   we proved 
                      eq
                        TList
                        TCons (lift h d t) (TApp (lifts h d t0) (lift h d v))
                        TCons (lift h d t) (TApp (lifts h d t0) (lift h d v))
                   by (eq_ind_r . . . previous . H)
                   we proved 
                      eq
                        TList
                        TCons (lift h d t) (lifts h d (TApp t0 v))
                        TCons (lift h d t) (TApp (lifts h d t0) (lift h d v))

                      eq
                        TList
                        lifts h d (TApp (TCons t t0) v)
                        TApp (lifts h d (TCons t t0)) (lift h d v)
          we proved 
             eq
               TList
               lifts h d (TApp vs v)
               TApp (lifts h d vs) (lift h d v)
       we proved 
          ∀h:nat
            .∀d:nat
              .∀v:T
                .∀vs:TList
                  .eq
                    TList
                    lifts h d (TApp vs v)
                    TApp (lifts h d vs) (lift h d v)