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