• Robbert Krebbers's avatar
    Make f_equiv slightly more robust. · 8e8305ce
    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.
    8e8305ce
tactics.v 20.6 KB