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

auto empty_member_false

empty_member_false: (all T:type. (all x:T. (x ∈ empty_set()) = false))

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

opaque define empty_set : (fn <T>  -> Set<T>) = generic T {
      fun  {
        char_fun(fun x:T { false })
      }
    }

auto empty_union

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

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

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

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

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

auto member_union_equal

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

opaque define operator ∈ : (fn <T> (T, Set<T>) -> bool) = generic T {
      fun x:T, S:Set<T> {
        rep(S)(x)
      }
    }

opaque define operator ∩ : (fn <T> (Set<T>, Set<T>) -> Set<T>) = generic T {
      fun P:Set<T>, Q:Set<T> {
        char_fun(fun x:T { (rep(P)(x) and rep(Q)(x)) })
      }
    }

opaque define operator ∪ : (fn <E> (Set<E>, Set<E>) -> Set<E>) = generic E {
      fun P:Set<E>, Q:Set<E> {
        char_fun(fun x:E { (rep(P)(x) or rep(Q)(x)) })
      }
    }

define operator ⊆ : (fn <T> (Set<T>, Set<T>) -> bool) = generic T {
      fun P:Set<T>, Q:Set<T> {
        (all x:T. (if x ∈ P then x ∈ Q))
      }
    }

opaque define rep : (fn <T> Set<T> -> (fn T -> bool)) = generic T {
      fun S:Set<T> {
        switch S {
          case char_fun(f) {
            f
          }
        }
      }
    }

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)

opaque define set_of_pred : (fn <T> (fn T -> bool) -> Set<T>) = generic T {
      fun f:(fn T -> bool) {
        char_fun(f)
      }
    }

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

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_fwd: (all T:type, f:(fn T -> bool), g:(fn T -> bool). (if set_of_pred(f) = set_of_pred(g) then f = g))

opaque define single : (fn <V> V -> Set<V>) = generic V {
      fun x:V {
        char_fun(fun y:V { x = y })
      }
    }

auto single_empty_false

single_empty_false: (all T:type, x:T. (single(x) = empty_set()) = false)

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

auto single_equal_equal

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

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

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

auto single_union_empty_false

single_union_empty_false: (all T:type, x:T, S:Set<T>. (single(x) ∪ S = empty_set()) = false)

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

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

auto union_empty

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

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

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

auto union_single_empty_false

union_single_empty_false: (all T:type, x:T, S:Set<T>. (S ∪ single(x) = empty_set()) = false)

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