DEFINITION nf2_iso_appls_lref()
TYPE =
       ∀c:C
         .∀i:nat
           .nf2 c (TLRef i)
             →∀vs:TList
                  .∀u:T
                    .pr3 c (THeads (Flat Appl) vs (TLRef i)) u
                      →iso (THeads (Flat Appl) vs (TLRef i)) u
BODY =
Show proof