DEFINITION ty3_nf2_inv_abst_premise_csort()
TYPE =
       ∀w:T.∀u:T.∀m:nat.(ty3_nf2_inv_abst_premise (CSort m) w u)
BODY =
        assume w: T
        assume u: T
        assume m: nat
          we must prove ty3_nf2_inv_abst_premise (CSort m) w u
          or equivalently 
                ∀d:C
                  .∀wi:T
                    .∀i:nat
                      .getl i (CSort m) (CHead d (Bind Abst) wi)
                        →∀vs:TList
                             .(pc3
                                 CSort m
                                 THeads (Flat Appl) vs (lift (S i) O wi)
                                 THead (Bind Abst) w u)
                               →False
           assume d: C
           assume wi: T
           assume i: nat
           suppose H: getl i (CSort m) (CHead d (Bind Abst) wi)
           assume vs: TList
           suppose : 
              pc3
                CSort m
                THeads (Flat Appl) vs (lift (S i) O wi)
                THead (Bind Abst) w u
             by (getl_gen_sort . . . H .)
             we proved False
          we proved 
             ∀d:C
               .∀wi:T
                 .∀i:nat
                   .getl i (CSort m) (CHead d (Bind Abst) wi)
                     →∀vs:TList
                          .(pc3
                              CSort m
                              THeads (Flat Appl) vs (lift (S i) O wi)
                              THead (Bind Abst) w u)
                            →False
          that is equivalent to ty3_nf2_inv_abst_premise (CSort m) w u
       we proved ∀w:T.∀u:T.∀m:nat.(ty3_nf2_inv_abst_premise (CSort m) w u)