Nate used Vars.liftn in fix_to_elim. I think this is in the kernel, but maybe a similar function is exposed elsewhere. Not sure if it's what we want. For now going to move all of the client code to use our shifting functions, but then at some point move our shifting functions to point to the predefined Coq functions when possible.
Nate used Vars.liftn in fix_to_elim. I think this is in the kernel, but maybe a similar function is exposed elsewhere. Not sure if it's what we want. For now going to move all of the client code to use our shifting functions, but then at some point move our shifting functions to point to the predefined Coq functions when possible.