Forked from
Iris / Iris
4778 commits behind the upstream repository.
-
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`.
