DEFINITION pr0_gen_lref()
TYPE =
       ∀x:T.∀n:nat.(pr0 (TLRef n) x)→(eq T x (TLRef n))
BODY =
Show proof