DEFINITION cimp()
TYPE =
       C→C→Prop
BODY =
λc1:C
         .λc2:C
           .∀b:B
             .∀d1:C
               .∀w:T
                 .∀h:nat
                   .getl h c1 (CHead d1 (Bind b) w)
                     →ex C λd2:C.getl h c2 (CHead d2 (Bind b) w)