DEFINITION sc3_abbr()
TYPE =
       ∀g:G
         .∀a:A
           .∀vs:TList
             .∀i:nat
               .∀d:C
                 .∀v:T
                   .∀c:C
                     .sc3 g a c (THeads (Flat Appl) vs (lift (S i) O v))
                       →(getl i c (CHead d (Bind Abbr) v)
                            →sc3 g a c (THeads (Flat Appl) vs (TLRef i)))
BODY =
Show proof