Skip to content
Snippets Groups Projects
Forked from Iris / Iris
Source project has a limited visibility.
user avatar
Robbert Krebbers authored
When having H : ▷ (P -∗ Q) and H2 : ▷ P, iSpecialize ("H" with "H2")
distributes the later over the wand.
e5a3be94
History
Name Last commit Last update