DEFINITION pc3_gen_appls_lref_sort()
TYPE =
       ∀c:C
         .∀d:C
           .∀v:T
             .∀i:nat
               .getl i c (CHead d (Bind Abst) v)
                 →∀vs:TList
                      .∀ws:TList
                        .∀n:nat
                          .(pc3
                              c
                              THeads (Flat Appl) vs (TLRef i)
                              THeads (Flat Appl) ws (TSort n))
                            →False
BODY =
Show proof