diff --git a/dicts/dicts.gobra b/dicts/dicts.gobra
new file mode 100644
index 0000000..ddbb3bb
--- /dev/null
+++ b/dicts/dicts.gobra
@@ -0,0 +1,489 @@
+/*
+  This file is part of gobra-libs which is released under the MIT license.
+  See LICENSE or go to https://github.com/viperproject/gobra-libs/blob/main/LICENSE
+  for full license details.
+
+  This file is inspired by the standard libraries and axiomatisations of the following verifiers:
+  - dafny-lang/dafny: https://github.com/dafny-lang/dafny/blob/master/Source/DafnyStandardLibraries/src/Std/Collections/Map.dfy
+  - verus-lang/verus:
+    - https://github.com/verus-lang/verus/blob/main/source/pervasive/map_lib.rs
+    - https://github.com/verus-lang/verus/blob/main/source/pervasive/map.rs
+  - viperproject/silicon: https://github.com/viperproject/silicon/blob/master/src/main/resources/dafny_axioms/maps.vpr
+  - why3:
+    - https://www.why3.org/stdlib/fmap.html
+    - https://www.why3.org/stdlib/map.html
+*/
+
+// This package defines lemmas for mathematical maps (aka dictionaries) commonly used
+// in specifications.
+package dicts
+
+import "util"
+import "sets"
+
+// A dictionary is empty if its domain is empty.
+ghost
+decreases
+pure func IsEmpty(d dict[int]int) bool {
+	return sets.IsEmpty(domain(d))
+}
+
+// Returns the empty dictionary.
+ghost
+ensures IsEmpty(result)
+decreases
+pure func Empty() (result dict[int]int) {
+	return dict[int]int{}
+}
+
+// Retrieves the value associated with the key, if present, as an option.
+ghost
+decreases
+pure func Get(d dict[int]int, k int) option[int] {
+	return k in domain(d) ? some(d[k]) : none[int]
+}
+
+// Keep all key-value pairs corresponding to the set of keys provided.
+ghost
+opaque
+ensures forall x int :: {result[x]} (x in domain(d) && x in xs) ==>
+	(x in domain(result) && result[x] == d[x])
+ensures forall x int :: {x in domain(result)} x in domain(result) ==>
+	(x in domain(d) && x in xs)
+ensures domain(result) == xs intersection domain(d)
+decreases xs
+pure func Restrict(d dict[int]int, xs set[int]) (result dict[int]int) {
+	return let ys := (xs intersection domain(d)) in
+		(sets.IsEmpty(ys) ? Empty() :
+			(let y := sets.Choose(ys) in
+			(let yr := sets.Remove(ys, y) in
+			(let _ := sets.IntersectLenUpper(xs, domain(d)) in
+			 Restrict(d, yr)[y = d[y]]))))
+}
+
+// Remove all key-value pairs corresponding to the set of keys provided.
+ghost
+decreases
+pure func RemoveKeys(d dict[int]int, xs set[int]) (result dict[int]int) {
+	return Restrict(d, domain(d) setminus xs)
+}
+
+// Remove a key-value pair. Returns d if k is not in the domain of d.
+ghost
+ensures len(result) <= len(d)
+ensures k in domain(d) ==> len(result) == len(d) - 1
+ensures !(k in domain(d)) ==> len(result) == len(d)
+decreases
+pure func Remove(d dict[int]int, k int) (result dict[int]int) {
+	return let ys := (sets.Remove(domain(d), k)) in
+		let _ := util.Asserting(ys intersection domain(d) == ys) in
+		RemoveKeys(d, sets.SingletonSet(k))
+}
+
+// True iff k maps to the same value or is not in the domains of d1 and d2.
+ghost
+decreases
+pure func IsEqualOnKey(d1, d2 dict[int]int, k int) bool {
+	return !(k in domain(d1) || k in domain(d2)) ||
+		(k in domain(d1) && k in domain(d2) && d1[k] == d2[k])
+}
+
+// True iff if d1 is a subset of d2.
+ghost
+decreases
+pure func IsSubset(d1, d2 dict[int]int) bool {
+	return domain(d1) subset domain(d2) &&
+		forall k int :: {IsEqualOnKey(d1, d2, k)} {k in domain(d1)} (k in domain(d1)) ==>
+		IsEqualOnKey(d1, d2, k)
+}
+
+// Union of two dictionaries. Does not require disjoint domains: on the intersection,
+// values from the second dictionary are chosen.
+ghost
+opaque
+ensures domain(result) == domain(d1) union domain(d2)
+ensures forall k int :: {result[k]} (k in domain(d2)) ==> result[k] == d2[k]
+ensures forall k int :: {result[k]}  (!(k in domain(d2)) && k in domain(d1)) ==>
+	result[k] == d1[k]
+decreases domain(d1) union domain(d2)
+pure func Union(d1, d2 dict[int]int) (result dict[int]int) {
+	return let ks := domain(d1) union domain(d2) in
+		(sets.IsEmpty(ks) ? Empty() :
+			let k := sets.Choose(ks) in
+			let c1 := Remove(d1, k) in
+			let c2 := Remove(d2, k) in
+			let _ := sets.RemoveUnionLen(domain(d1), domain(d2), k) in
+			(k in domain(d2) ? Union(c1, c2)[k = d2[k]] : Union(c1, c2)[k = d1[k]]))
+}
+
+// Dictionaries are disjoint iff their domains are disjoint.
+ghost
+decreases
+pure func AreDisjoint(d1, d2 dict[int]int) bool {
+	return sets.AreDisjoint(domain(d1), domain(d2))
+}
+
+// The length of the union of two disjoint dictionaries is the sum of each of their lengths.
+ghost
+opaque
+requires AreDisjoint(d1, d2)
+ensures len(Union(d1, d2)) == len(d1) + len(d2)
+decreases
+pure func DisjointUnionLen(d1, d2 dict[int]int) util.Unit {
+	return util.Unit{}
+}
+
+// True iff a dictionary is injective.
+ghost
+opaque
+decreases
+pure func IsInjective(d dict[int]int) bool {
+	return forall k1, k2 int :: {d[k1], d[k2]} (k1 != k2 && k1 in domain(d) && k2 in domain(d)) ==>
+		d[k1] != d[k2]
+}
+
+// True iff a dictionary contains all valid keys.
+ghost
+opaque
+decreases
+pure func IsTotal(d dict[int]int) bool {
+	return forall k int :: {d[k]} {k in domain(d)} k in domain(d)
+}
+
+// True iff a dictionary is monotonic.
+ghost
+opaque
+decreases
+pure func IsMonotonic(d dict[int]int) bool {
+	return forall k1, k2 int :: {d[k1], d[k2]} (k1 in domain(d) && k2 in domain(d) && k1 <= k2) ==>
+		d[k1] <= d[k2]
+}
+
+// True iff a dictionary is monotonic. Only considers keys greater than or equal to start.
+ghost
+opaque
+decreases
+pure func IsMonotonicFrom(d dict[int]int, start int) bool {
+	return forall k1, k2 int :: {d[k1], d[k2]} (k1 in domain(d) && k2 in domain(d) && start <= k1 && k1 <= k2) ==>
+		d[k1] <= d[k2]
+}
+
+// True iff a dictionary is monotonic. Only considers keys in the interval [start, end).
+ghost
+opaque
+decreases
+pure func IsMonotonicFromTo(d dict[int]int, start, end int) bool {
+	return forall k1, k2 int :: {d[k1], d[k2]} (k1 in domain(d) &&
+						    k2 in domain(d) &&
+		 				    start <= k1 && k1 <= k2 && k2 < end) ==> d[k1] <= d[k2]
+}
+
+// True iff two dictionaries are equal in the interval [start, end).
+ghost
+opaque
+decreases
+pure func IsEqualInRange(d1, d2 dict[int]int, start, end int) bool {
+	return forall k int :: {d1[k], d2[k]} {k in domain(d1)} {k in domain(d2)}(start <= k && k < end) ==>
+		k in domain(d1) && k in domain(d2) && d1[k] == d2[k]
+}
+
+// True iff d1 and d2 agree on all keys that their domains share.
+ghost
+decreases
+pure func Agree(d1, d2 dict[int]int) bool {
+	return forall k int :: {d1[k], d2[k]} k in (domain(d1) intersection domain(d2)) ==>
+		d1[k] == d2[k]
+}
+
+// The domain of a map after removing a key is equivalent to removing
+// the key from the domain of the original map.
+ghost
+opaque
+ensures domain(Remove(d, k)) == sets.Remove(domain(d), k)
+decreases
+pure func RemoveDomain(d dict[int]int, k int) util.Unit {
+	return util.Unit{}
+}
+
+// The domain of the empty dictionary is the empty set.
+ghost
+opaque
+requires IsEmpty(d)
+ensures domain(d) == sets.Empty()
+decreases
+pure func EmptyDictEmptyDomain(d dict[int]int) util.Unit {
+	return util.Unit{}
+}
+
+// The domain of a dictionary after inserting a key-value pair is equivalent to
+// inserting the key into the original map's domain set.
+ghost
+opaque
+ensures domain(d[k = v]) == sets.Add(domain(d), k)
+decreases
+pure func InsertDomain(d dict[int]int, k, v int) util.Unit {
+	return util.Unit{}
+}
+
+// Inserting value at k in d results in a dictionary that maps k to v.
+ghost
+opaque
+ensures d[k = v][k] == v
+decreases
+pure func UpdateSame(d dict[int]int, k, v int) util.Unit {
+	return util.Unit{}
+}
+
+// Reassigning the corresponding value to a key does not change the dictionary.
+ghost
+opaque
+requires k in domain(d)
+requires v == d[k]
+ensures d[k = v] == d
+decreases
+pure func UpdateEqual(d dict[int]int, k, v int) util.Unit {
+	return util.Unit{}
+}
+
+// Inserting v at k2 does not change the value mapped to by any other keys in d.
+ghost
+opaque
+requires k1 != k2
+ensures k2 in domain(d[k1 = v]) == k2 in domain(d)
+ensures k2 in domain(d) ==> d[k1 = v][k2] == d[k2]
+decreases
+pure func UpdateDifferent(d dict[int]int, k1, k2, v int) util.Unit {
+	return util.Unit{}
+}
+
+// Removing a key-value pair from a dictionary does not change the value mapped to
+// by any other keys in the map.
+ghost
+opaque
+requires k1 in domain(d)
+requires k1 != k2
+ensures Remove(d, k2)[k1] == d[k1]
+decreases
+pure func RemoveDifferent(d dict[int]int, k1, k2 int) util.Unit {
+	return util.Unit{}
+}
+
+// Two maps are equivalent if their domains are equivalent and every key in their
+// domains map to the same value.
+ghost
+opaque
+ensures (d1 == d2) ==
+	(domain(d1) == domain(d2) && forall k int :: {d1[k], d2[k]} k in domain(d1) ==>	d1[k] == d2[k])
+decreases
+pure func ExtEqual(d1, d2 dict[int]int) util.Unit {
+	return util.Unit{}
+}
+
+// The cardinality of a dictionary is non-negative.
+ghost
+opaque
+ensures len(d) >= 0
+decreases
+pure func NonNegativeLen(d dict[int]int) util.Unit {
+	return util.Unit{}
+}
+
+// The cardinality of a dictionary is equal to the cardinality of its domain.
+ghost
+opaque
+ensures len(d) == len(domain(d))
+decreases
+pure func DomainLenEq(d dict[int]int) util.Unit {
+	return util.Unit{}
+}
+
+// If two dictionaries are disjoint there is no key that is in both of their domains.
+ghost
+opaque
+requires AreDisjoint(d1, d2)
+ensures !(k in domain(d1) && k in domain(d2))
+decreases
+pure func DisjointNoSharedKey(d1, d2 dict[int]int, k int) util.Unit {
+	return util.Unit{}
+}
+
+// If two dictionaries are not disjoint, there exists a key that is in both of their domains.
+ghost
+opaque
+requires !AreDisjoint(d1, d2)
+ensures exists k int :: {k in domain(d1), k in domain(d2)} k in domain(d1) && k in domain(d2)
+decreases
+pure func NotDisjointSharedKey(d1, d2 dict[int]int) util.Unit {
+	return util.Unit{}
+}
+
+// There is only one empty map.
+ghost
+opaque
+requires IsEmpty(d)
+ensures d == Empty()
+decreases
+pure func EmptyIsUnique(d dict[int]int) util.Unit {
+	return util.Unit{}
+}
+
+// An empty dictionary contains no keys.
+ghost
+opaque
+requires IsEmpty(d)
+ensures !(k in domain(d))
+decreases
+pure func NotInEmpty(d dict[int]int, k int) util.Unit {
+	return util.Unit{}
+}
+
+// There exists a key in a non-empty dictionary.
+ghost
+opaque
+requires !IsEmpty(d)
+ensures exists k int :: {k in domain(d)} k in domain(d)
+decreases
+pure func NotEmptyKeyExists(d dict[int]int, k int) util.Unit {
+	return util.Unit{}
+}
+
+// If a key is in d, d is not empty.
+ghost
+opaque
+requires k in domain(d)
+ensures !IsEmpty(d)
+decreases
+pure func KeyInDomainDictNotEmpty(d dict[int]int, k int) util.Unit {
+	return util.Unit{}
+}
+
+// Inserting a new key increases the cardinality of the dictionary by 1.
+// Updating the value of a key does not change the cardinality.
+ghost
+opaque
+ensures k in domain(d) ==> len(d[k = v]) == len(d)
+ensures !(k in domain(d)) ==> len(d[k = v]) == len(d) + 1
+decreases
+pure func InsertUpdateLen(d dict[int]int, k, v int) util.Unit {
+	return util.Unit{}
+}
+
+// If a value is in the range of a dictionary, there exists a corresponding key.
+ghost
+opaque
+requires v in range(d)
+ensures exists k int :: {k in domain(d)} k in domain(d) && d[k] == v
+decreases
+pure func ValueHasKey(d dict[int]int, v int) util.Unit {
+	return util.Unit{}
+}
+
+// If a value is in the domain of a dictionary, the corresponding value is in its range.
+ghost
+opaque
+requires k in domain(d)
+ensures d[k] in range(d)
+decreases
+pure func KeyMapsToRange(d dict[int]int, k int) util.Unit {
+	return util.Unit{}
+}
+
+// Returns a dictionary with the values at k1 and k2 swapped.
+ghost
+requires k1 in domain(d) && k2 in domain(d)
+ensures domain(result) == domain(d)
+ensures result[k1] == d[k2] && result[k2] == d[k1]
+ensures forall k int :: {result[k]} (k in domain(d) && k != k1 && k != k2) ==>
+	result[k] == d[k]
+decreases
+pure func Swap(d dict[int]int, k1, k2 int) (result dict[int]int) {
+	return d[k1 = d[k2]][k2 = d[k1]]
+}
+
+// Returns the set of keys from the given dictionary that map to the specified value.
+ghost
+opaque
+ensures forall k int :: {k in result} (k in domain(d) && d[k] == v) == (k in result)
+decreases len(d)
+pure func Keys(d dict[int]int, v int) (result set[int]) {
+	return IsEmpty(d) ? sets.Empty() :
+		(let x := sets.Choose(domain(d)) in
+		(let subKeys := Keys(Remove(d, x), v) in
+		(d[x] == v ? sets.Add(subKeys, x) : subKeys)))
+	
+}
+
+// Returns the number of occurences of the value in the dictionary.
+ghost
+decreases
+pure func Occurrences(d dict[int]int, v int) int {
+	return len(Keys(d, v))
+}
+
+// Remove preserves the injectivity of a dictionary.
+ghost
+opaque
+requires IsInjective(d)
+ensures IsInjective(Remove(d, k))
+decreases
+pure func RemovePreservesInjectivity(d dict[int]int, k int) util.Unit {
+	return let _ := reveal IsInjective(d) in
+		let _ := reveal IsInjective(Remove(d, k)) in
+		util.Unit{}
+}
+
+// After removing a key, the corresponding value occurs one less time.
+ghost
+opaque
+requires k in domain(d)
+ensures Occurrences(Remove(d, k), d[k]) == Occurrences(d, d[k]) - 1
+decreases
+pure func RemoveOccurrences(d dict[int]int, k int) util.Unit {
+	return let ks1 := reveal Keys(d, d[k]) in
+	let ks2 := reveal Keys(Remove(d, k), d[k]) in
+	util.Asserting(ks2 == sets.Remove(ks1, k))
+}
+
+// Adding a new key-value pair increases the occurrence of the value by one.
+ghost
+opaque
+requires !(k in domain(d))
+ensures Occurrences(d[k = v], v) == Occurrences(d, v) + 1
+decreases
+pure func AddOccurrences(d dict[int]int, k, v int) util.Unit {
+	return let ks1 := reveal Keys(d, v) in
+		let ks2 := reveal Keys(d[k = v], v) in
+		util.Asserting(ks2 == sets.Add(ks1, k))
+}
+
+// Updating a key to a new value results in an additional occurrences for the
+// new value, and one less occurrence for the old value.
+ghost
+opaque
+requires k in domain(d)
+requires v != d[k]
+ensures Occurrences(d[k = v], v) == Occurrences(d, v) + 1
+ensures Occurrences(d[k = v], d[k]) == Occurrences(d, d[k]) - 1
+decreases
+pure func UpdateOccurrences(d dict[int]int, k, v int) util.Unit {
+	return let ks1v := reveal Keys(d, v) in
+		let ks2v := reveal Keys(d[k = v], v) in
+		let _ := util.Asserting(ks2v == sets.Add(ks1v, k)) in
+		let ks1dk := reveal Keys(d, d[k]) in
+		let ks2dk := reveal Keys(d[k = v], d[k]) in
+		util.Asserting(ks2dk == sets.Remove(ks1dk, k))
+}
+
+// v can occur at most once as a value in injective dictionaries.
+ghost
+opaque
+requires IsInjective(d)
+ensures Occurrences(d, v) <= 1
+decreases len(d)
+pure func InjectiveOccurrences(d dict[int]int, v int) util.Unit {
+	return Occurrences(d, v) <= 1 ? util.Unit{} :
+		let x1 := sets.Choose(Keys(d, v)) in
+		let x2 := sets.Choose(sets.Remove(Keys(d, v), x1)) in
+		let _ := reveal IsInjective(d) in
+		util.Unit{}
+}
diff --git a/gomap/gomap.gobra b/gomap/gomap.gobra
new file mode 100644
index 0000000..fc92223
--- /dev/null
+++ b/gomap/gomap.gobra
@@ -0,0 +1,169 @@
+/*
+  This file is part of gobra-libs which is released under the MIT license.
+  See LICENSE or go to https://github.com/viperproject/gobra-libs/blob/main/LICENSE
+  for full license details.
+*/
+
+// This package defines Go maps and their associated operations in terms of
+// mathematical maps (dictionaries).
+package gomap
+
+import "dicts"
+import "sets"
+import "util"
+
+// Converts a Go map to a mathematical map (dictionary).
+//
+// This function is abstract since at the moment there is no good way to
+// iteratively create a dictionary from a map: using Go's range would
+// require us to update the dict in the loop which isn't possible. Calling
+// ToDict recursively by creating a submap of m would have side-effects,
+// which isn't possible in a pure function.
+ghost
+requires acc(m, _)
+ensures domain(result) == domain(m)
+ensures forall k int :: {result[k]} {k in domain(m)} k in domain(m) ==> result[k] == m[k]
+decreases
+pure func ToDict(m map[int]int) (result dict[int]int)
+
+// A map is empty if its length is 0.
+ghost
+requires acc(m, _)
+ensures result == dicts.IsEmpty(ToDict(m))
+decreases
+pure func IsEmpty(m map[int]int) (result bool) {
+	return len(m) == 0
+}
+
+// Retrieves the value associated with the key, if present, as an option.
+ghost
+requires acc(m, _)
+decreases
+pure func GetOption(m map[int]int, k int) (result option[int]) {
+	return dicts.Get(ToDict(m), k)
+}
+
+// True iff k maps to the same value or is not in the domains of m1 and m2.
+ghost
+requires acc(m1, _)
+requires acc(m2, _)
+ensures result == dicts.IsEqualOnKey(ToDict(m1), ToDict(m2), k)
+decreases
+pure func IsEqualOnKey(m1, m2 map[int]int, k int) (result bool) {
+	return !(k in domain(m1) || k in domain(m2)) ||
+		(k in domain(m1) && k in domain(m2) && m1[k] == m2[k])
+}
+
+// True iff m1 is a subset of m2.
+ghost
+requires acc(m1, _)
+requires acc(m2, _)
+ensures result == dicts.IsSubset(ToDict(m1), ToDict(m2))
+decreases
+pure func IsSubset(m1, m2 map[int]int) (result bool) {
+	return domain(m1) subset domain(m2) &&
+			forall k int :: {IsEqualOnKey(m1, m2, k)} {k in domain(m1)} (k in domain(m1)) ==>
+				IsEqualOnKey(m1, m2, k)
+}
+
+// Maps are disjoint iff their domains are disjoint.
+ghost
+requires acc(m1, _)
+requires acc(m2, _)
+ensures result == dicts.AreDisjoint(ToDict(m1), ToDict(m2))
+decreases
+pure func AreDisjoint(m1, m2 map[int]int) (result bool) {
+	return sets.AreDisjoint(domain(m1), domain(m2))
+}
+
+ghost
+opaque
+requires acc(m, _)
+ensures result == dicts.IsInjective(ToDict(m))
+decreases
+pure func IsInjective(m map[int]int) (result bool) {
+	return let _ := reveal dicts.IsInjective(ToDict(m)) in
+		forall k1, k2 int :: {m[k1], m[k2]} (k1 != k2 && k1 in domain(m) && k2 in domain(m)) ==>
+			m[k1] != m[k2]
+}
+
+ghost
+opaque
+requires acc(m, _)
+ensures result == dicts.IsMonotonic(ToDict(m))
+decreases
+pure func IsMonotonic(m map[int]int) (result bool) {
+	return let _ := reveal dicts.IsMonotonic(ToDict(m)) in
+		forall k1, k2 int :: {m[k1], m[k2]} (k1 in domain(m) && k2 in domain(m) && k1 <= k2) ==>
+			m[k1] <= m[k2]
+}
+
+// True iff a map is monotonic in the range [start, +∞)
+ghost
+opaque
+requires acc(m, _)
+ensures result == dicts.IsMonotonicFrom(ToDict(m), start)
+decreases
+pure func IsMonotonicFrom(m map[int]int, start int) (result bool) {
+	return let _ := reveal dicts.IsMonotonicFrom(ToDict(m), start) in
+		forall k1, k2 int :: {m[k1], m[k2]} (k1 in domain(m) && k2 in domain(m) && start <= k1 && k1 <= k2) ==>
+			m[k1] <= m[k2]
+}
+
+// True iff a map is monotonic in the interval [start, end).
+ghost
+opaque
+requires acc(m, _)
+ensures result == dicts.IsMonotonicFromTo(ToDict(m), start, end)
+decreases
+pure func IsMonotonicFromTo(m map[int]int, start, end int) (result bool) {
+	return let _ := reveal dicts.IsMonotonicFromTo(ToDict(m), start, end) in
+		forall k1, k2 int :: {m[k1], m[k2]} (k1 in domain(m) &&
+						     k2 in domain(m) &&
+		 				     start <= k1 && k1 <= k2 && k2 < end) ==>
+							m[k1] <= m[k2]
+}
+
+// True iff two maps are equal in the interval [start, end).
+ghost
+opaque
+requires acc(m1, _)
+requires acc(m2, _)
+ensures result == dicts.IsEqualInRange(ToDict(m1), ToDict(m2), start, end)
+decreases
+pure func IsEqualInRange(m1, m2 map[int]int, start, end int) (result bool) {
+	return let _ := reveal dicts.IsEqualInRange(ToDict(m1), ToDict(m2), start, end) in
+		(forall k int :: {m1[k], m2[k]} {k in domain(m1)} {k in domain(m2)} (start <= k && k < end) ==>
+			k in domain(m1) && k in domain(m2) && m1[k] == m2[k])
+}
+
+// True iff m1 and m2 agree on all keys that their domains share.
+ghost
+requires acc(m1, _)
+requires acc(m2, _)
+ensures result == dicts.Agree(ToDict(m1), ToDict(m2))
+decreases
+pure func Agree(m1, m2 map[int]int) (result bool) {
+	return forall k int :: {m1[k], m2[k]} k in (domain(m1) intersection domain(m2)) ==>
+			m1[k] == m2[k]
+}
+
+// Returns the set of keys from m that map to the specified value.
+ghost
+requires acc(m, _)
+ensures forall k int :: {k in result} (k in domain(m) && m[k] == v) == (k in result)
+decreases len(m)
+pure func Keys(m map[int]int, v int) (result set[int]) {
+	// Since we don't have access to Remove for gomaps, we define this
+	// using ToDict. Note the lack of opaque in the function.
+	return dicts.Keys(ToDict(m), v)
+}
+
+// Returns the number of occurences of the value in the map.
+ghost
+requires acc(m, _)
+ensures result == dicts.Occurrences(ToDict(m), v)
+decreases
+pure func Occurrences(m map[int]int, v int) (result int) {
+	return len(Keys(m, v))
+}
diff --git a/sets/sets.gobra b/sets/sets.gobra
index a7d2eed..c001f12 100644
--- a/sets/sets.gobra
+++ b/sets/sets.gobra
@@ -72,7 +72,7 @@ requires e in xs
 ensures xs == SingletonSet(e)
 decreases
 pure func SingletonIsSingletonSet(xs set[int], e int) util.Unit {
-	return let _ := choose(xs) in util.Unit{}
+	return let _ := Choose(xs) in util.Unit{}
 }
 
 // Elements in a singleton set are equal to each other.
@@ -83,7 +83,7 @@ requires b in xs
 ensures a == b
 decreases
 pure func SingletonEquality(xs set[int], a int, b int) util.Unit {
-	return let _ := choose(xs) in util.Unit{}
+	return let _ := Choose(xs) in util.Unit{}
 }
 
 // Constructs a set with all integers in the range [a, b).
@@ -114,7 +114,7 @@ ensures forall i int :: {i # result} (!(i in s)) ==> ((i # result) == 0)
 decreases s
 pure func ToMultiset(s set[int]) (result mset[int]) {
 	return IsEmpty(s) ? mset[int] {} :
-		let x := choose(s) in
+		let x := Choose(s) in
 		((mset[int] {}) union (mset[int] {x})) union ToMultiset(Remove(s, x))
 }
 
@@ -124,7 +124,7 @@ requires !IsEmpty(xs)
 ensures e in xs
 ensures IsSingleton(xs) ==> xs == SingletonSet(e)
 decreases
-pure func choose(xs set[int]) (e int)
+pure func Choose(xs set[int]) (e int)
 
 // Returns whether xs and ys are disjoint sets.
 ghost
@@ -373,10 +373,10 @@ pure func SubsetLen(xs, ys set[int]) util.Unit {
 	return (!(xs subset ys) || len(xs) == 0) ? util.Unit{} :
 		len(xs) == len(ys) ?
 			let _ := SubsetEquality(xs, ys) in
-			(let e := choose(xs) in
+			(let e := Choose(xs) in
 			(SubsetLen(Remove(xs, e), Remove(ys, e)))) :
 
-			let e:= choose(xs) in
+			let e:= Choose(xs) in
 			(SubsetLen(Remove(xs, e), Remove(ys, e)))			
 }
 
@@ -388,7 +388,7 @@ ensures len(xs union ys) >= len(ys)
 decreases ys
 pure func UnionLenLower(xs, ys set[int]) util.Unit {
 	return IsEmpty(ys) ? util.Unit{} :
-		let y := choose(ys) in
+		let y := Choose(ys) in
 		(let yr := Remove(ys, y) in
 		(y in xs ?
 			(let xr := Remove(xs, y) in
@@ -412,7 +412,7 @@ ensures len(xs intersection ys) <= len(xs)
 decreases xs
 pure func IntersectLenUpper(xs, ys set[int]) util.Unit {
 	return IsEmpty(xs) ? util.Unit{} :
-		let x := choose(xs) in
+		let x := Choose(xs) in
 		(let _ := util.Asserting((Remove(xs, x)) intersection ys == Remove((xs intersection ys), x)) in
 		(IntersectLenUpper(Remove(xs, x), ys)))
 }
@@ -446,7 +446,7 @@ ghost
 ensures (e in xs) ==> (len(Add(xs, e)) == len(xs))
 ensures !(e in xs) ==> (len(Add(xs, e)) == len(xs) + 1)
 decreases
-func AddLen(xs set[int], e int) util.Unit {
+pure func AddLen(xs set[int], e int) util.Unit {
 	return util.Unit{}
 }
 
@@ -456,10 +456,27 @@ ghost
 ensures (e in xs) ==> (len(Remove(xs, e)) == len(xs) - 1)
 ensures !(e in xs) ==> (len(Remove(xs, e)) == len(xs))
 decreases
-func RemoveLen(xs set[int], e int) util.Unit {
+pure func RemoveLen(xs set[int], e int) util.Unit {
 	return util.Unit{}
 }
 
+// Remove is right distributive over union.
+ghost
+ensures Remove(xs union ys, e) == Remove(xs, e) union Remove(ys, e)
+decreases
+pure func RemoveUnion(xs, ys set[int], e int) util.Unit {
+	return util.Unit{}
+}
+
+// If e is in (xs union ys), removing it from both sets reduces the cardinality by 1.
+ghost
+requires e in (xs union ys)
+ensures len(Remove(xs, e) union Remove(ys, e)) == len(xs union ys) - 1
+decreases
+pure func RemoveUnionLen(xs, ys set[int], e int) util.Unit {
+	return RemoveUnion(xs, ys, e)
+}
+
 // If xs and ys are disjoint, the cardinality of their union is equal to the
 // sum of the cardinality of xs, and the cardinality of ys.
 ghost
diff --git a/util/util.gobra b/util/util.gobra
index 6703a81..2357870 100644
--- a/util/util.gobra
+++ b/util/util.gobra
@@ -1,4 +1,3 @@
-
 // Copyright 2023 ETH Zurich
 //
 // Licensed under the Apache License, Version 2.0 (the "License");
@@ -23,7 +22,9 @@ const Uncallable bool = false
 ghost
 requires false
 decreases
-func Unreachable() { }
+pure func Unreachable() Unit {
+	return Unit{}
+}
 
 ghost
 ensures false