Forked from
Iris / Iris
Source project has a limited visibility.
-
Robbert Krebbers authored
It now first turns hypotheses `X ∪ Y ⊆ Z` into `X ⊆ Z` and `Y ⊆ Z`.
Robbert Krebbers authoredIt now first turns hypotheses `X ∪ Y ⊆ Z` into `X ⊆ Z` and `Y ⊆ Z`.
