Am I using Z3Py correctly? I'm concerned at how similar the proofs look

[LivInTheLookingGlass]

I currently have a repo with a bunch of different definitions of the same sequence. I've been trying to use Z3 to help prove that they all produce the same sequence, but I'm having a problem. All of the proofs it produces are eerily similar, with only a few exceptions.

I have no idea if I'm using this tool correctly, and I would love it if someone could help me figure that out. My workflow essentially is as follows:

1. Collect each definition by calling to_z3() in the appropriate module, which constructs a RecFunction that encodes the series generator
2. Gather each pairwise combination
3. For each of them, apply the following constraints, where n is an index in the sequence and s_ref is the base I'm outputting the sequence in:

• solver.add(ForAll(n, Implies(n >= 0, T1(n) == T2(n))))
• (new as of today) solver.add(ForAll(n, Implies(And(n >= 0, n < s_ref), And(T1(n) == n, T2(n) == n))))
• (new as of today) solver.add(T1(s_ref) == 1, T2(s_ref) == 1)

4. Run each of these, saving the output of solver.proof()

Is this reasonable/correct usage?