+let rec shift f c t = match c with
+ | ESort -> f t
+ | EBind (e, a, b) -> add_bind (shift f e) a b t
+ | EAppl (e, a, v) -> add_appl (shift f e) a v t
+ | EProj (e, a, d) -> add_proj (shift f e) a d t
+
+let rec append f c = function
+ | ESort -> f c
+ | EBind (e, a, b) -> append (push_bind f a b) c e
+ | EAppl (e, a, t) -> append (push_appl f a t) c e
+ | EProj (e, a, d) -> append (push_proj f a d) c e
+
+let resolve_lref err f id lenv =
+ let rec aux i = function
+ | ESort -> err ()
+ | EAppl (tl, _, _) -> aux i tl
+ | EBind (tl, a, _) ->
+ let f id0 _ = if id0 = id then f i else aux (succ i) tl in
+ E.name err f a
+ | EProj (tl, _, d) -> append (aux i) tl d
+ in
+ aux 0 lenv
+
+let rec get_name err f i = function
+ | ESort -> err i
+ | EAppl (tl, _, _) -> get_name err f i tl
+ | EBind (_, a, _) when i = 0 ->
+ let err () = err i in
+ E.name err f a
+ | EBind (tl, _, _) -> get_name err f (pred i) tl
+ | EProj (tl, _, e) ->
+ let err i = get_name err f i tl in
+ get_name err f i e