Forked from
Iris / Iris
Source project has a limited visibility.
-
Robbert Krebbers authored
This enables things like `iSpecialize ("H2" with "H1") in the below: "H1" : P ---------□ "H2" : □ P -∗ Q ---------∗ RRobbert Krebbers authoredThis enables things like `iSpecialize ("H2" with "H1") in the below: "H1" : P ---------□ "H2" : □ P -∗ Q ---------∗ R
