DEFINITION csubc_drop_conf_O()
TYPE =
       ∀g:G
         .∀c1:C
           .∀e1:C
             .∀h:nat
               .(drop h O c1 e1)→∀c2:C.(csubc g c1 c2)→(ex2 C λe2:C.drop h O c2 e2 λe2:C.csubc g e1 e2)
BODY =
Show proof