Factor out Constructor.v from ObAxioms.v