add some union_with lemmas

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 lookup_union on maps.

• 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_with is 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.