• Robbert Krebbers's avatar
    Tweak boxes. · f2bf449c
    Robbert Krebbers authored
    No longer `put box_own_prop γ P` in the invariant, it is persistent.
    f2bf449c
boxes.v 11.7 KB