- | B.Sort h ->
- let f h = f x (B.Sort h) in H.apply f g h
- | B.LRef i ->
- let f = function
- | Some (_, B.Abst w) -> f x w
- | Some (_, B.Abbr (B.Cast (w, v))) -> f x w
- | Some (_, B.Abbr _) -> assert false
- | Some (_, B.Void) ->
+ | B.Sort (a, h) ->
+ let f h = f x (B.Sort (a, h)) in H.apply f g h
+ | B.LRef (_, i) ->
+ let f _ = function
+ | Some (_, B.Abst w) ->
+ S.lift (f x) (succ i) (0) w
+ | Some (_, B.Abbr (B.Cast (_, w, _))) ->
+ S.lift (f x) (succ i) (0) w
+ | Some (_, B.Abbr _) -> assert false
+ | Some (_, B.Void) ->