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