DEFINITION nf2_appls_lref()
TYPE =
       ∀c:C
         .∀i:nat
           .nf2 c (TLRef i)
             →∀vs:TList.(nfs2 c vs)→(nf2 c (THeads (Flat Appl) vs (TLRef i)))
BODY =
Show proof