Forked from
Iris / Iris
3077 commits behind the upstream repository.
Robbert Krebbers
authored
Soundness lemma for internal equality of `uPred`. See merge request iris/iris!315
| Name | Last commit | Last update |
|---|---|---|
| .. | ||
| lib | ||
| base_logic.v | ||
| bi.v | ||
| bupd_alt.v | ||
| derived.v | ||
| proofmode.v | ||
| upred.v | ||