I have this coq file, for example aFile.v, that has a bunch of definitions and parameters and axioms and lemmas, some depending on each other. So for example, let’s say aFile.v looks something like this:

`Definition def1 := .. Parameter param1 :=.. Definition def2 :=.. (* uses parameters & definitions from above *) Axiom ax1 :.. (* uses parameters & definitions from above *) Lemma lem1: (* uses parameters & definitions from above *)`

Is there a way to turn this file into something like a module that I can instantiate in other coq files in a way that allows me to define the parameters and prove the axioms in this instantiation?

I tried turning it into a module type, but then when I tried instantiating it I had to basically write down all the definitions again, otherwise I’d get an error. I want something similar to this but where I only define `Parameter`

s and prove `Axiom`

s, and any `Definition`

s or `Lemma`

s are just imported as is.