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 =
        assume g: G
        assume c: C
        assume d: C
        assume v: T
        assume i: nat
        suppose H: getl i c (CHead d (Bind Abbr) v)
        assume w: T
        suppose H0: sty1 g d v w
          we proceed by induction on H0 to prove sty1 g c (TLRef i) (lift (S i) O w)
             case sty1_sty0 : t2:T H1:sty0 g d v t2 ⇒
                the thesis becomes sty1 g c (TLRef i) (lift (S i) O t2)
                   by (sty0_abbr . . . . . H . H1)
                   we proved sty0 g c (TLRef i) (lift (S i) O t2)
                   by (sty1_sty0 . . . . previous)
sty1 g c (TLRef i) (lift (S i) O t2)
             case sty1_sing : t:T :sty1 g d v t t2:T H3:sty0 g d t t2 ⇒
                the thesis becomes sty1 g c (TLRef i) (lift (S i) O t2)
                (H2) by induction hypothesis we know sty1 g c (TLRef i) (lift (S i) O t)
                   by (getl_drop . . . . . H)
                   we proved drop (S i) O c d
                   by (sty0_lift . . . . H3 . . . previous)
                   we proved sty0 g c (lift (S i) O t) (lift (S i) O t2)
                   by (sty1_sing . . . . H2 . previous)
sty1 g c (TLRef i) (lift (S i) O t2)
          we proved sty1 g c (TLRef i) (lift (S i) O w)
       we proved 
          ∀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))