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