DEFINITION csubt_getl_abst()
TYPE =
       ∀g:G
         .∀c1:C
           .∀d1:C
             .∀t:T
               .∀n:nat
                 .getl n c1 (CHead d1 (Bind Abst) t)
                   →∀c2:C
                        .csubt g c1 c2
                          →(or
                               ex2 C λd2:C.csubt g d1 d2 λd2:C.getl n c2 (CHead d2 (Bind Abst) t)
                               ex4_2
                                 C
                                 T
                                 λd2:C.λ:T.csubt g d1 d2
                                 λd2:C.λu:T.getl n c2 (CHead d2 (Bind Abbr) u)
                                 λ:C.λu:T.ty3 g d1 u t
                                 λd2:C.λu:T.ty3 g d2 u t)
BODY =
Show proof