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