DEFINITION ty3_nf2_gen__ty3_nf2_inv_abst_aux()
TYPE =
       ∀c:C
         .∀w1:T
           .∀u1:T
             .ty3_nf2_inv_abst_premise c w1 u1
               →∀t:T
                    .∀w2:T
                      .∀u2:T
                        .(pc3
                            c
                            THead (Flat Appl) t (THead (Bind Abst) w2 u2)
                            THead (Bind Abst) w1 u1)
                          →ty3_nf2_inv_abst_premise c w2 u2
BODY =
Show proof