DEFINITION csuba_gen_abst()
TYPE =
       ∀g:G
         .∀d1:C
           .∀c:C
             .∀u1:T
               .csuba g (CHead d1 (Bind Abst) u1) c
                 →(or
                      ex2 C λd2:C.eq C c (CHead d2 (Bind Abst) u1) λd2:C.csuba g d1 d2
                      ex4_3
                        C
                        T
                        A
                        λd2:C.λu2:T.λ:A.eq C c (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