DEFINITION pc3_gen_appls_lref_abst()
TYPE =
       ∀c:C
         .∀d:C
           .∀v:T
             .∀i:nat
               .getl i c (CHead d (Bind Abst) v)
                 →∀vs:TList
                      .∀w:T
                        .∀u:T
                          .(pc3
                              c
                              THeads (Flat Appl) vs (TLRef i)
                              THead (Bind Abst) w u)
                            →False
BODY =
Show proof