DEFINITION csuba_gen_abbr()
TYPE =
       ∀g:G
         .∀d1:C
           .∀c:C
             .∀u:T
               .csuba g (CHead d1 (Bind Abbr) u) c
                 →ex2 C λd2:C.eq C c (CHead d2 (Bind Abbr) u) λd2:C.csuba g d1 d2
BODY =
Show proof