DEFINITION csuba_getl_abst()
TYPE =
       ∀g:G
         .∀c1:C
           .∀d1:C
             .∀u1:T
               .∀i:nat
                 .getl i c1 (CHead d1 (Bind Abst) u1)
                   →∀c2:C
                        .csuba g c1 c2
                          →(or
                               ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
                               ex4_3
                                 C
                                 T
                                 A
                                 λd2:C.λu2:T.λ:A.getl i c2 (CHead d2 (Bind Abbr) u2)
                                 λd2:C.λ:T.λ:A.csuba g d1 d2
                                 λ:C.λ:T.λa:A.arity g d1 u1 (asucc g a)
                                 λd2:C.λu2:T.λa:A.arity g d2 u2 a)
BODY =
Show proof