DEFINITION sc3_lift()
TYPE =
       ∀g:G
         .∀a:A
           .∀e:C
             .∀t:T
               .(sc3 g a e t)→∀c:C.∀h:nat.∀d:nat.(drop h d c e)→(sc3 g a c (lift h d t))
BODY =
Show proof