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