DEFINITION lref_map()
TYPE =
       (nat→nat)→nat→T→T
BODY =
Show proof