DEFINITION drop1_csubc_trans()
TYPE =
       ∀g:G
         .∀hds:PList
           .∀c2:C.∀e2:C.(drop1 hds c2 e2)→∀e1:C.(csubc g e2 e1)→(ex2 C λc1:C.drop1 hds c1 e1 λc1:C.csubc g c2 c1)
BODY =
Show proof