-
Robbert Krebbers authored
This enables things like `iSpecialize ("H2" with "H1") in the below: "H1" : P ---------□ "H2" : □ P -∗ Q ---------∗ R
2821e99e
This enables things like `iSpecialize ("H2" with "H1") in the below: "H1" : P ---------□ "H2" : □ P -∗ Q ---------∗ R