Imports in `core` and friends

[MevenBertrand]

The current solution of blindly copying the core, unscoped, etc. files is unsatisfactory: unscoped uses

Require Import core.

but this invocation will only work unqualified in certain scenarios.

Moreover, the -f command-line option, to force overwrite of the output files, does not make a difference between these imported files and the generated file. This complicates the scenario where one wants a command to regenerate the auto-generated file, but keep modified core & friends (for instance, to circumvent the above problem by patching the first line).

I'm not sure what the best solution is (for now, I'll probably just solve the issue on my side). But since we added the option of having a custom header for the generated files exactly for this sort of case, we probably want also a more flexible approach for this one in the long run.