opaque union Set<T>

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

fun set_of_pred<T>(f:(fn T -> bool)) {
  char_fun(f)
}

fun empty_set<T>() {
  
}

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

single_pred: (all T:type. (all x:T. set_of_pred(fun y:T { x = y }) = single(x)))

empty_no_members: (all T:type. (all x:T. not (x  empty_set())))

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

rep_set_of_pred: (all T:type, f:(fn T -> bool). rep(set_of_pred(f)) = f)

set_of_pred_equal_fwd: (all T:type, f:(fn T -> bool), g:(fn T -> bool). (if set_of_pred(f) = set_of_pred(g) then f = g))

set_of_pred_equal_bkwd: (all T:type, f:(fn T -> bool), g:(fn T -> bool). (if f = g then set_of_pred(f) = set_of_pred(g)))

set_of_pred_equal: (all T:type, f:(fn T -> bool), g:(fn T -> bool). ((set_of_pred(f) = set_of_pred(g))  (f = g)))

member_set_of_pred: (all T:type, x:T, f:(fn T -> bool). (if x  set_of_pred(f) then f(x)))

union_set_of_pred: (all T:type, f:(fn T -> bool), g:(fn T -> bool). set_of_pred(f)  set_of_pred(g) = set_of_pred(fun x { (f(x) or g(x)) }))

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  empty_set() = A))

empty_union: (all T:type. (all A:Set<T>. @empty_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)))

member_equal: (all T:type, A:Set<T>, B:Set<T>. (if (all x:T. ((x  A)  (x  B))) then A = B))