DEFINITION sc3_lift1()
TYPE =
       ∀g:G
         .∀e:C.∀a:A.∀hds:PList.∀c:C.∀t:T.(sc3 g a e t)→(drop1 hds c e)→(sc3 g a c (lift1 hds t))
BODY =
Show proof