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