DEFINITION sty1_lift()
TYPE =
       ∀g:G
         .∀e:C
           .∀t1:T
             .∀t2:T
               .sty1 g e t1 t2
                 →∀c:C.∀h:nat.∀d:nat.(drop h d c e)→(sty1 g c (lift h d t1) (lift h d t2))
BODY =
Show proof