union MultiSet<T>

fun cnt<T>(M:MultiSet<T>)

auto cnt_empty

cnt_empty: (all T:type. (all x:T. cnt(@m_empty<T>())(x) = 0))

cnt_equal: (all T:type, A:MultiSet<T>, B:MultiSet<T>. (if cnt(A) = cnt(B) then A = B))

auto cnt_equal_equal

cnt_equal_equal: (all T:type, A:MultiSet<T>, B:MultiSet<T>. (cnt(A) = cnt(B)) = (A = B))

auto cnt_one

cnt_one: (all T:type. (all x:T. cnt(m_one(x))(x) = 1))

cnt_sum: (all T:type. (all A:MultiSet<T>, B:MultiSet<T>, x:T. cnt(A ⨄ B)(x) = cnt(A)(x) + cnt(B)(x)))

auto empty_m_sum

empty_m_sum: (all T:type. (all A:MultiSet<T>. @m_empty<T>() ⨄ A = A))

fun m_empty<T>()

fun m_one<T>(x:T)

m_sum_assoc: (all T:type. (all A:MultiSet<T>, B:MultiSet<T>, C:MultiSet<T>. (A ⨄ B) ⨄ C = A ⨄ (B ⨄ C)))

m_sum_commutes: (all T:type. (all A:MultiSet<T>, B:MultiSet<T>. A ⨄ B = B ⨄ A))

auto m_sum_empty

m_sum_empty: (all T:type. (all A:MultiSet<T>. A ⨄ @m_empty<T>() = A))

fun operator ⨄<T>(P:MultiSet<T>, Q:MultiSet<T>)

fun set_of_mset<T>(M) {
  set_of_pred(fun x { (if cnt(M)(x) = 0 then false else true) })
}

som_empty: (all T:type. set_of_mset(@m_empty<T>()) = @empty_set<T>())

som_one_single: (all T:type. (all x:T. set_of_mset(m_one(x)) = single(x)))

som_union: (all T:type. (all A:MultiSet<T>, B:MultiSet<T>. set_of_mset(A ⨄ B) = set_of_mset(A) ∪ set_of_mset(B)))