Make `union_Some` a ``, add `union_None` and `union_is_Some`.

This makes it more consistent with other Some lemmas, that are also bidirectional.

See also the discussion !466 (comment 91517)

The change to union_Some is not backwards compatible, so we need to either provide a new lemma (with a new name, but what?) for the → direction, or we need to update existing code. It's not clear to me how much union_Some is used in reverse dependencies.

Shouldn't these be union_Some_iff or so? Looking at union_Some_{l,r}, those are very different lemmas from union_Some.

resolved all threads

The change to union_Some is not backwards compatible, so we need to either provide a new lemma (with a new name, but what?) for the → direction, or we need to update existing code. It's not clear to me how much union_Some is used in reverse dependencies.

It is not used in the rev deps we track at all. So, I am fine with changing it.

added 16 commits

• 9675a293...1f83a259 - 13 commits from branch master
• 1d1769bf - Make `union_Some` a ``.
• 0aa55b25 - Add `union_None` and `union_is_Some`.
• 1c3c4b79 - CHANGELOG.

Compare with previous version

enabled an automatic merge when the pipeline for 1c3c4b79 succeeds

@iris-users:

• Strengthen union_Some to become a biimplication.

merged

mentioned in commit 385d29dd