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