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