DEFINITION sn3_appls_abbr()
TYPE =
       ∀c:C
         .∀d:C
           .∀w:T
             .∀i:nat
               .getl i c (CHead d (Bind Abbr) w)
                 →∀vs:TList
                      .sn3 c (THeads (Flat Appl) vs (lift (S i) O w))
                        →sn3 c (THeads (Flat Appl) vs (TLRef i))
BODY =
Show proof