DEFINITION lref_map()
TYPE =
       (nat→nat)→nat→T→T
BODY =
FIXlref_map{
         lref_map:(nat→nat)→nat→T→T
         :=λf:nat→nat
           .λd:nat
             .λt:T
               .<λt1:T.T>
                 CASE t OF
                   TSort n⇒TSort n
                 | TLRef i⇒TLRef <λb:bool.nat> CASE blt i d OF true⇒i | false⇒f i
                 | THead k u t0⇒THead k (lref_map f d u) (lref_map f (s k d) t0)
         }