Factored out of !478 (merged)
added 1 commit
Compare with previous version
enabled an automatic merge when the pipeline for 35797f91 succeeds
Going to merge, this makes the lemma strictly more general.
merged
mentioned in commit b4e387e6
@iris-users
Equivalence
PreOrder
set_fold_proper
This should make it easier to prove the premise.
