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 =
        assume c: C
        assume w1: T
        assume u1: T
          we must prove 
                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
          or equivalently 
                ∀d:C
                    .∀wi:T
                      .∀i:nat
                        .getl i c (CHead d (Bind Abst) wi)
                          →∀vs:TList
                               .(pc3
                                   c
                                   THeads (Flat Appl) vs (lift (S i) O wi)
                                   THead (Bind Abst) w1 u1)
                                 →False
                  →∀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
           suppose H: 
              ∀d:C
                .∀wi:T
                  .∀i:nat
                    .getl i c (CHead d (Bind Abst) wi)
                      →∀vs:TList
                           .(pc3
                               c
                               THeads (Flat Appl) vs (lift (S i) O wi)
                               THead (Bind Abst) w1 u1)
                             →False
           assume t: T
           assume w2: T
           assume u2: T
           suppose H0: 
              pc3
                c
                THead (Flat Appl) t (THead (Bind Abst) w2 u2)
                THead (Bind Abst) w1 u1
             we must prove ty3_nf2_inv_abst_premise c w2 u2
             or equivalently 
                   ∀d:C
                     .∀wi:T
                       .∀i:nat
                         .getl i c (CHead d (Bind Abst) wi)
                           →∀vs:TList
                                .(pc3
                                    c
                                    THeads (Flat Appl) vs (lift (S i) O wi)
                                    THead (Bind Abst) w2 u2)
                                  →False
              assume d: C
              assume wi: T
              assume i: nat
              suppose H1: getl i c (CHead d (Bind Abst) wi)
              assume vs: TList
              suppose H2: 
                 pc3
                   c
                   THeads (Flat Appl) vs (lift (S i) O wi)
                   THead (Bind Abst) w2 u2
                by (pc3_thin_dx . . . H2 . .)
                we proved 
                   pc3
                     c
                     THead
                       Flat Appl
                       t
                       THeads (Flat Appl) vs (lift (S i) O wi)
                     THead (Flat Appl) t (THead (Bind Abst) w2 u2)
                by (pc3_t . . . previous . H0)
                we proved 
                   pc3
                     c
                     THead
                       Flat Appl
                       t
                       THeads (Flat Appl) vs (lift (S i) O wi)
                     THead (Bind Abst) w1 u1
                that is equivalent to 
                   pc3
                     c
                     THeads (Flat Appl) (TCons t vs) (lift (S i) O wi)
                     THead (Bind Abst) w1 u1
                by (H . . . H1 . previous)
                we proved False
             we proved 
                ∀d:C
                  .∀wi:T
                    .∀i:nat
                      .getl i c (CHead d (Bind Abst) wi)
                        →∀vs:TList
                             .(pc3
                                 c
                                 THeads (Flat Appl) vs (lift (S i) O wi)
                                 THead (Bind Abst) w2 u2)
                               →False
             that is equivalent to ty3_nf2_inv_abst_premise c w2 u2
          we proved 
             ∀d:C
                 .∀wi:T
                   .∀i:nat
                     .getl i c (CHead d (Bind Abst) wi)
                       →∀vs:TList
                            .(pc3
                                c
                                THeads (Flat Appl) vs (lift (S i) O wi)
                                THead (Bind Abst) w1 u1)
                              →False
               →∀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
          that is equivalent to 
             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
       we proved 
          ∀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