• Amin Timany's avatar
    Prove binary soundness for Fμ,ref,par · c7a553d3
    Amin Timany authored
    There is one admit that needs to be taken care of. The admitted case is validity
    of a monoid element of iprod. At the moment iris doesn't seem to have necessary
    lemmas to prove this easily.
    c7a553d3
soundness_binary.v 12.8 KB