DEFINITION sty1_abbr()
TYPE =
       ∀g:G
         .∀c:C
           .∀d:C
             .∀v:T
               .∀i:nat
                 .getl i c (CHead d (Bind Abbr) v)
                   →∀w:T.(sty1 g d v w)→(sty1 g c (TLRef i) (lift (S i) O w))
BODY =
Show proof