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