DEFINITION nf2_lref_abst()
TYPE =
       ∀c:C
         .∀e:C
           .∀u:T.∀i:nat.(getl i c (CHead e (Bind Abst) u))→(nf2 c (TLRef i))
BODY =
Show proof