There is an old issue, that's related, why one should avoid using equality relations in AI used for creating a proof. It will go back and forth and fill the log with trivial statements before it comes to the right proof path. This might end up being the majority of the proof and could be an unbounded part. Then somebody has to read that and spend a good deal of time deciding what's trivial and what isn't. Whereas if you remove equality, you have something that isn't very natural.