• Dmitry Khalanskiy's avatar
    Add pair_op_1 and pair_op_2 · 902f5305
    Dmitry Khalanskiy authored
    The two new lemmas allow splitting the resources in one component
    of a pair when the other component has nothing. In combination
    with `pair_split`, they allow to arbitrarily split the resource
    `(a ⋅ a', b ⋅ b')`.
    
    This is in line with `prod_local_update_1` and
    `prod_local_update_2`, the lemmas that allow, in a sense, to only
    consider one component of a pair.
    902f5305
cmra.v 68.4 KB