DEFINITION iso_gen_lref()
TYPE =
       ∀u2:T.∀n1:nat.(iso (TLRef n1) u2)→(ex nat λn2:nat.eq T u2 (TLRef n2))
BODY =
Show proof