DEFINITION ty3_gen_abst_abst()
TYPE =
       ∀g:G
         .∀c:C
           .∀u:T
             .∀t1:T
               .∀t2:T
                 .ty3 g c (THead (Bind Abst) u t1) (THead (Bind Abst) u t2)
                   →ex2 T λw:T.ty3 g c u w λ:T.ty3 g (CHead c (Bind Abst) u) t1 t2
BODY =
Show proof