These are taken verbatim from Perennial, where they already existed and I just needed both of them. So there is clearly some need here.
But the lemmas are kind of weird so I am open for discussions for how to better provide them.
The first has a very specific lemma statement with this
λ x' _, Some x'. This arises from
The second is the same as
left_id, but never in a hundred years would I have realized I can use that LeftId instance.
union_withis not a binary operator; I think we need a readable lemma that shows up in
SearchAbout union_with None. Yes LeftId does show up in that search but I doubt many people will realize that it is useful in this situation -- I have skipped over it myself.
Basically: not everything that can be written as LeftId / RightId, should be written that way. IMO we should only use these classes for things that are actually binary operators, written with infix notation. I don't object to instances also existing in other cases, but those instances should only exist in addition to regular lemmas, not instead of them.