• Robbert Krebbers's avatar
    Make f_equiv slightly more robust. · 5d66333c
    Robbert Krebbers authored
    Now, for example, when having equiv (Some x) (Some y) it will
    try to find a Proper whose range is an equiv before hitting the
    eq instance. My hack is general enough that it works for Forall2,
    dist, and so on, too.
    5d66333c
boxes.v 8.29 KB