An error occurred while fetching the assigned milestone of the selected merge_request.
For other operations (empty, singleton) we have a similar lemma. This one is missing.
I had to move some things around in the file, and re-proved map_fmap_singleton_inv using the new lemma.