DEFINITION ty3_gen_lift()
TYPE =
       ∀g:G
         .∀c:C
           .∀t1:T
             .∀x:T
               .∀h:nat
                 .∀d:nat
                   .ty3 g c (lift h d t1) x
                     →∀e:C.(drop h d c e)→(ex2 T λt2:T.pc3 c (lift h d t2) x λt2:T.ty3 g e t1 t2)
BODY =
Show proof