• Robbert Krebbers's avatar
    Derived lifting lemmas. · a50d7b04
    Robbert Krebbers authored
    The proofs are neither short nor nice, but at least they compile
    fast (4 sec for the whole file) and the statements look like
    they would look like on paper.
    a50d7b04
hoare_lifting.v 5.87 KB