union Set<T> {
  char_fun((fn T -> bool))
}

fun rep<T>(S:Set<T>) {
  switch S {
    case char_fun(f) {
      f
    }
  }
}

fun single<V>(x:V) {
  char_fun(fun y:V { x = y })
}

fun operator ∪<E>(P:Set<E>, Q:Set<E>) {
  char_fun(fun x:E { (rep(P)(x) or rep(Q)(x)) })
}

fun operator ∩<T>(P:Set<T>, Q:Set<T>) {
  char_fun(fun x:T { (rep(P)(x) and rep(Q)(x)) })
}

fun operator ∈<T>(x:T, S:Set<T>) {
  rep(S)(x)
}

fun operator ⊆<T>(P:Set<T>, Q:Set<T>) {
  (all x:T. (if x ∈ P then x ∈ Q))
}

single_member: (all T:type. (all x:T. x ∈ single(x)))

single_equal: (all T:type. (all x:T, y:T. (if y ∈ single(x) then x = y)))

single_equal_equal: (all T:type. (all x:T, y:T. (y ∈ single(x)) = (x = y)))

empty_no_members: (all T:type. (all x:T. not (x ∈ ∅)))

rep_char_fun: (all T:type, f:(fn T -> bool). rep(char_fun(f)) = f)

union_member: (all T:type. (all x:T, A:Set<T>, B:Set<T>. (if (x ∈ A or x ∈ B) then x ∈ A ∪ B)))

member_union: (all T:type. (all x:T, A:Set<T>, B:Set<T>. (if x ∈ A ∪ B then (x ∈ A or x ∈ B))))

member_union_equal: (all T:type. (all x:T, A:Set<T>, B:Set<T>. (x ∈ A ∪ B) = (x ∈ A or x ∈ B)))

union_empty: (all T:type. (all A:Set<T>. A ∪ ∅ = A))

empty_union: (all T:type. (all A:Set<T>. ∅ ∪ A = A))

union_sym: (all T:type. (all A:Set<T>, B:Set<T>. A ∪ B = B ∪ A))

union_assoc: (all T:type. (all A:Set<T>, B:Set<T>, C:Set<T>. (A ∪ B) ∪ C = A ∪ (B ∪ C)))

in_left_union: (all T:type. (all B:Set<T>. (all x:T, A:Set<T>. (if x ∈ A then x ∈ A ∪ B))))

in_right_union: (all T:type. (all A:Set<T>. (all x:T, B:Set<T>. (if x ∈ B then x ∈ A ∪ B))))

subset_equal: (all T:type. (all A:Set<T>, B:Set<T>. (if (A ⊆ B and B ⊆ A) then A = B)))