DEFINITION csubv_clear_conf()
TYPE =
       ∀c1:C
         .∀c2:C
           .csubv c1 c2
             →∀b1:B
                  .∀d1:C
                    .∀v1:T
                      .clear c1 (CHead d1 (Bind b1) v1)
                        →ex2_3 B C T λ:B.λd2:C.λ:T.csubv d1 d2 λb2:B.λd2:C.λv2:T.clear c2 (CHead d2 (Bind b2) v2)
BODY =
Show proof