I went down this road a long time ago, for a different reason. There are classic "axioms" for arrays, first written down by John McCarthy.[1][2] Those are classically considered to be axioms. But I set out to prove them via constructive means.

I was using the Boyer-Moore theorem prover, which starts from something close to Peano arithmetic and builds up number theory from there. In Boyer-Moore theory, everything is represented as a LISP S-expression. Equality is defined as as the expressions being identical.

So, in Boyer-Moore theory, you have ordered lists, but not sets. A set, remember, can be informally defined as a collection in which each item appears exactly once. The order of the items doesn't matter.

In Boyer-Moore theory, short of forcing in a new axiom, which risks soundness, there's no way to say "the order of the items doesn't matter". At startup, there's no notion of a "set". But you can build one up via definitions and theorems.

So I started by defining an array as an list of (subscript, value) tuples, ordered by subscript. Two arrays are equal if they are both valid and identical.

So, given that definition, we can write the classic "axioms" for arrays as statements to be proven. First,
we define "storea(A,I,V)" as the function that stores into an array in a functional sense - it
creates a new array where element I has been replaced with V. And we define the predicate "arrayp", which tests whether an array is properly constructed.

The key "axiom" for arrays, in Boyer-Moore notation, reads:

(PROVE-LEMMA SELECT-OF-STORE (REWRITE)
(IMPLIES (AND (arrayp A) (NUMBERP I) (NUMBERP J))
(EQUAL (selecta (storea A I V) J)
(IF (EQUAL I J) V (selecta A J)))))

That means, if A is an array, and I and J are integers, then, for all A, I, and J:

storea(A,I,V)[J] = (if i=j then V else A[J])

So that's McCarthy's key axiom for arrays.

It's not an axiom here. It's a lemma to be proven. It turns out that with the right
sequence of lemmas, that statement can be proved as a theorem. Here's that sequence.[3]
I wrote that around 1981, and it went through the Boyer-Moore theorem prover. So we could then load those statements into the Oppen-Nelson simplifier (what today is called a SAT solver) as safely proven rewrite rules. This established that the array theory was both sound and consistent between the two provers.

A few years back, I revived the original Boyer-Moore theorem prover, converted it to GNU Common LISP, and put it on Github.[4] You can download it, run it, and run the set of rules in [3] through it to get the proofs.
(That took about 45 minutes of VAX time in 1981. Now it takes about a second.)

The proofs are long, because there's a lot of case analysis. Arrays are ordered lists of tuples in this theory, and there's a lot of detail about maintaining that order. We had to prove

(PROVE-LEMMA STORE-IS-PROPER (REWRITE) (EQUAL (arrayp (storea A I V)) T))

which proves that the storing operation always produces a validly ordered array. That's essentially a code proof of correctness for a recursive function The Boyer-Moore prover was able to grind out a proof of that without help. That was a long proof, too.

I submitted this to JACM. It was rejected, mostly for uglyness. The concept that you needed all this heavy machine-driven case analysis to prove a nice simple "axiom" upset mathematicians. Today it would be less of an issue. People are now more used to proofs that take a lot of grinding through cases.

You could build up set theory this way, via ordered lists, if you wanted.

So that's a classic of what happens if you take "equal" seriously.

[1] http://www-formal.stanford.edu/jmc/towards.pdf

[2] https://theory.stanford.edu/~arbrad/papers/arrays.pdf

[3] https://github.com/John-Nagle/pasv/blob/master/src/work/temp...

[4] https://github.com/John-Nagle/nqthm