DEFINITION csuba_getl_abbr()
TYPE =
       ∀g:G
         .∀c1:C
           .∀d1:C
             .∀u:T
               .∀i:nat
                 .getl i c1 (CHead d1 (Bind Abbr) u)
                   →∀c2:C
                        .csuba g c1 c2
                          →ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
BODY =
Show proof