Lambda calculus (created in the 1930s by Church) allows identity to be assigned arbitrarily and changed at any time.
When we make ontologies / taxinomies that’s also what we do.
Naming categories, assigning symbols, it’s all the same act of stating (or asserting equivalence).
To prove it? It’s asserted. I think of a first-order prover like so:
Similar to creating a maze with each turn a transformation within the logical statement and asking only one question:
Can I get back to the entrance from the entrance?
If you can it’s proven.