+
+let get_index err f i j lenv =
+ let rec aux f i k = function
+ | ESort -> err i
+ | EBind (tl, _, Abst [])
+ | EBind (tl, _, Abbr [])
+ | EBind (tl, _, Void 0) -> aux f i k tl
+ | EBind (_, a, _) when i = 0 ->
+ if Entity.count_names a > j then f (k + j) else err i
+ | EBind (tl, a, _) ->
+ aux f (pred i) (k + Entity.count_names a) tl
+ | EProj _ -> assert false (* TODO *)
+ in
+ aux f i 0 lenv