DEFINITION ty3_nf2_inv_abst()
TYPE =
       ∀g:G
         .∀c:C
           .∀t:T
             .∀w:T
               .∀u:T
                 .ty3 g c t (THead (Bind Abst) w u)
                   →(nf2 c t
                        →(nf2 c w
                             →(ty3_nf2_inv_abst_premise c w u
                                  →(ex4_2
                                       T
                                       T
                                       λv:T.λ:T.eq T t (THead (Bind Abst) w v)
                                       λ:T.λw0:T.ty3 g c w w0
                                       λv:T.λ:T.ty3 g (CHead c (Bind Abst) w) v u
                                       λv:T.λ:T.nf2 (CHead c (Bind Abst) w) v))))
BODY =
Show proof