opaque union MultiSet<T>

fun cnt<T>(M:MultiSet<T>) {
  switch M {
    case m_fun(f) {
      f
    }
  }
}

fun m_empty<T>() {
  m_fun(fun y:T { 0 })
}

fun m_one<T>(x:T) {
  m_fun(fun y:T { (if x = y then 1 else 0) })
}

fun operator ⨄<T>(P:MultiSet<T>, Q:MultiSet<T>) {
  m_fun(fun x:T { cnt(P)(x) + cnt(Q)(x) })
}

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

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)))

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

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

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

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

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

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)))