Forked from
Iris / stdpp
Source project has a limited visibility.
-
Robbert Krebbers authored
Turn `x ∈ X` only into `0 < multiplicity x X` at leaves of `∈` to enable better first-order reasoning.
Robbert Krebbers authoredTurn `x ∈ X` only into `0 < multiplicity x X` at leaves of `∈` to enable better first-order reasoning.