(* PARALLEL R-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES ****************)
definition lfpr: sh → genv → relation3 term lenv lenv ≝
(* PARALLEL R-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES ****************)
definition lfpr: sh → genv → relation3 term lenv lenv ≝