DEFINITION sty0_gen_lref()
TYPE =
       ∀g:G
         .∀c:C
           .∀x:T
             .∀n:nat
               .sty0 g c (TLRef n) x
                 →(or
                      ex3_3
                        C
                        T
                        T
                        λe:C.λu:T.λ:T.getl n c (CHead e (Bind Abbr) u)
                        λe:C.λu:T.λt:T.sty0 g e u t
                        λ:C.λ:T.λt:T.eq T x (lift (S n) O t)
                      ex3_3
                        C
                        T
                        T
                        λe:C.λu:T.λ:T.getl n c (CHead e (Bind Abst) u)
                        λe:C.λu:T.λt:T.sty0 g e u t
                        λ:C.λu:T.λ:T.eq T x (lift (S n) O u))
BODY =
Show proof