Strange behavior of `elem_of_singleton` in Coq 8.12
Given
Hk_is_i : k ∈ {[i]}
with Coq 8.12, running apply elem_of_singleton in Hk_is_i
now produces mapset_car {[i]} !! k ∈ {[Some ()]}
instead of the expected k = i
. No idea how that is possible...