This generalizes Fix_unfold to a setoid setting. In particular, we can use this to unfold multi-argument fixpoints without requiring functional extensionality.
