1 に答える
This is a shot in the dark without seeing the whole development, but sometimes, when you can't see a difference, it means that there's a difference in a part you don't see. Namely, implicit arguments.
For example, you might have an implicit argument somewhere that appears identically in two locations in the working proof attempt, and that appears in two distinct but interconvertible (or even merely equal) in the non-working proof attempt. Occasionally tactics require identical terms to fire up, whereas interconvertible terms would suffice with the same proof tree, and equal terms would suffice with judicious introduction of eq_refl. When you're working with high-level tactics such as the setoid tactics, it can be difficult to understand what's going on under the hood.
Try comparing the situations under Set Printing Implicit or Set Printing All, or working with No Strict Implicit or No Implicit Arguments for a small part of the proof.