DEFINITION csubv_drop_conf()
TYPE =
       ∀c1:C
         .∀c2:C
           .(csubv c1 c2)→∀e1:C.∀h:nat.(drop h O c1 e1)→(ex2 C λe2:C.csubv e1 e2 λe2:C.drop h O c2 e2)
BODY =
Show proof