• Ralf Jung's avatar
    Add support for ElimInv to introduce a binder from the accessor · b2711d60
    Ralf Jung authored
    If the accessor introduces a binder, the first Coq-level intro pattern of `iInv`
    is used for that binder unless the type of the binder is unit, in which case
    `iInv` removes it completely.  Binders on the closing view shift are not (yet)
    supported as they are harder to smoothly eliminate in the unit case.
    b2711d60
cancelable_invariants.v 3.72 KB