DEFINITION csuba_drop_abst_rev()
TYPE =
       ∀i:nat
         .∀c1:C
           .∀d1:C
             .∀u:T
               .drop i O c1 (CHead d1 (Bind Abst) u)
                 →∀g:G
                      .∀c2:C
                        .csuba g c2 c1
                          →(or
                               ex2 C λd2:C.drop i O c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d2 d1
                               ex2_2 C T λd2:C.λu2:T.drop i O c2 (CHead d2 (Bind Void) u2) λd2:C.λ:T.csuba g d2 d1)
BODY =
Show proof