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