DEFINITION pr2_gen_lref()
TYPE =
       ∀c:C
         .∀x:T
           .∀n:nat
             .pr2 c (TLRef n) x
               →(or
                    eq T x (TLRef n)
                    ex2_2
                      C
                      T
                      λd:C.λu:T.getl n c (CHead d (Bind Abbr) u)
                      λ:C.λu:T.eq T x (lift (S n) O u))
BODY =
Show proof