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