union MultiSet<T> {
  m_fun((fn T -> Nat))
}

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

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_m_fun: (all T:type, f:(fn T -> Nat). cnt(m_fun(f)) = f)

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

m_empty_zero: (all T:type. (all x:T. cnt(m_fun(fun y:T { 0 }))(x) = 0))

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

m_sum_empty: (all T:type. (all A:MultiSet<T>. A ⨄ m_fun(fun y:T { 0 }) = A))

empty_m_sum: (all T:type. (all A:MultiSet<T>. m_fun(fun x:T { 0 }) ⨄ 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) {
  char_fun(fun x { (if cnt(M)(x) = 0 then false else true) })
}

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