Weird unfolding by `cbn` with `gset`
Consider the following code.
From stdpp Require Import gmap.
Goal ∀ (k : Z) (s : gset Z), {[k]} ∪ s = s ∪ {[k]} ∪ {[k]}.
cbn. (* <-- weird unfolding. *)
Evaluating the cbn
tactic turns the goal into:
∀ (k : Z) (s : gset Z), (let (m2) := s in {| mapset.mapset_car := {[k := ()]} ∪ m2 |}) = s ∪ {[k]} ∪ {[k]}
which is not what I was expecting. Why does this unfolding take place?