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.
