Finite maps over
multisets of sigma types
lifting from alist
Fold a commutative function over the key-value pairs in the map
sdiff s s' consists of all key-value pairs from
s' where the keys are in
s' but not both.
s₁ ∪ s₂ is the key-based union of two finite maps. It is left-biased: if
there exists an
a ∈ s₁,
lookup a (s₁ ∪ s₂) = lookup a s₁.