DEFINITION csubt_drop_abbr()
TYPE =
       ∀g:G
         .∀n:nat
           .∀c1:C
             .∀c2:C
               .csubt g c1 c2
                 →∀d1:C
                      .∀u:T
                        .drop n O c1 (CHead d1 (Bind Abbr) u)
                          →ex2 C λd2:C.csubt g d1 d2 λd2:C.drop n O c2 (CHead d2 (Bind Abbr) u)
BODY =
Show proof