@@ -266,7 +266,8 @@ irTerm vs env tm@(App f a) = case unApply tm of
266 -- otherwise, just apply the name
266 -- otherwise, just apply the name
267 _ -> applyName n ist args
267 _ -> applyName n ist args
269+ -- turn de bruijn vars into regular named references and try again
269− (V i, args) -> irTerm vs env (P Bound (env !! i) Erased)
270+ (V i, args) -> irTerm vs env $ mkApp (P Bound (env !! i) Erased) args
271 (f, args)
272 (f, args)
272 -> LApp False
273 -> LApp False