DEFINITION sn3_abbr()
TYPE =
       ∀c:C
         .∀d:C
           .∀v:T
             .∀i:nat
               .getl i c (CHead d (Bind Abbr) v)
                 →(sn3 d v)→(sn3 c (TLRef i))
BODY =
Show proof