DEFINITION csubt_gen_abst()
TYPE =
       ∀g:G
         .∀e1:C
           .∀c2:C
             .∀v1:T
               .csubt g (CHead e1 (Bind Abst) v1) c2
                 →(or
                      ex2 C λe2:C.eq C c2 (CHead e2 (Bind Abst) v1) λe2:C.csubt g e1 e2
                      ex4_2 C T λe2:C.λv2:T.eq C c2 (CHead e2 (Bind Abbr) v2) λe2:C.λ:T.csubt g e1 e2 λ:C.λv2:T.ty3 g e1 v2 v1 λe2:C.λv2:T.ty3 g e2 v2 v1)
BODY =
Show proof