DEFINITION cimp_getl_conf()
TYPE =
       ∀c1:C
         .∀c2:C
           .cimp c1 c2
             →∀b:B
                  .∀d1:C
                    .∀w:T
                      .∀i:nat
                        .getl i c1 (CHead d1 (Bind b) w)
                          →ex2 C λd2:C.cimp d1 d2 λd2:C.getl i c2 (CHead d2 (Bind b) w)
BODY =
Show proof