DEFINITION nf2_appl_lref()
TYPE =
       ∀c:C
         .∀u:T
           .nf2 c u
             →∀i:nat.(nf2 c (TLRef i))→(nf2 c (THead (Flat Appl) u (TLRef i)))
BODY =
Show proof