DEFINITION csubv_clear_conf_void()
TYPE =
       ∀c1:C
         .∀c2:C
           .csubv c1 c2
             →∀d1:C
                  .∀v1:T
                    .clear c1 (CHead d1 (Bind Void) v1)
                      →ex2_2 C T λd2:C.λ:T.csubv d1 d2 λd2:C.λv2:T.clear c2 (CHead d2 (Bind Void) v2)
BODY =
Show proof