This would require a hash input (or combination of inputs) to be unique over a limited / expected domain, right?

I mean, you could take anything as an axiom so there are no real requirements for it.

I would imagine you would want to demonstrate the P(collision|domain+operating lifetime) << acceptable level or risk, and after you’d done that, take the uniqueness of hashes as a axiom for the proof system?

That’s just speculation on my part, since I haven’t done much with formal proofs of working code

No you just special case the function call and tell the proof analyzer "this never happens". Strictly speaking, a lie, but probably a sophisticated prover could even be rigged to keep track of those conditions (not in x years, e.g.) if you so chose