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 =
Show proof