DEFINITION arity_gen_lref()
TYPE =
       ∀g:G
         .∀c:C
           .∀i:nat
             .∀a:A
               .arity g c (TLRef i) a
                 →(or
                      ex2_2 C T λd:C.λu:T.getl i c (CHead d (Bind Abbr) u) λd:C.λu:T.arity g d u a
                      ex2_2
                        C
                        T
                        λd:C.λu:T.getl i c (CHead d (Bind Abst) u)
                        λd:C.λu:T.arity g d u (asucc g a))
BODY =
Show proof