• Robbert Krebbers's avatar
    Theorems about big_ops for uPred. · 5726049c
    Robbert Krebbers authored
    Also, specialize the big ops to gmap and gset because that is all that
    we are using. For the big ops on sets this also means we can use Leibniz
    equality on sets.
    5726049c
upred_big_op.v 8.37 KB