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