• Johannes Kloos's avatar
    Unfolding lemma for Fix in setoids. · 04b92602
    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
relations.v 9.68 KB