DEFINITION ty3_nf2_inv_abst_premise()
TYPE =
       C→T→T→Prop
BODY =
λc:C
         .λw:T
           .λu:T
             .∀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) w u)
                            →False