DEFINITION sn3_appls_lref()
TYPE =
       ∀c:C
         .∀i:nat
           .nf2 c (TLRef i)
             →∀us:TList.(sns3 c us)→(sn3 c (THeads (Flat Appl) us (TLRef i)))
BODY =
Show proof