DEFINITION ty3_gen_appl_nf2()
TYPE =
       ∀g:G
         .∀c:C
           .∀w:T
             .∀v:T
               .∀x:T
                 .ty3 g c (THead (Flat Appl) w v) x
                   →(ex4_2
                        T
                        T
                        λu:T.λt:T.pc3 c (THead (Flat Appl) w (THead (Bind Abst) u t)) x
                        λu:T.λt:T.ty3 g c v (THead (Bind Abst) u t)
                        λu:T.λ:T.ty3 g c w u
                        λu:T.λt:T.nf2 c (THead (Bind Abst) u t))
BODY =
Show proof