DEFINITION nf2_gen_lref()
TYPE =
       ∀c:C
         .∀d:C
           .∀u:T
             .∀i:nat
               .getl i c (CHead d (Bind Abbr) u)
                 →(nf2 c (TLRef i))→∀P:Prop.P
BODY =
Show proof