var S, T : Type

type Bool;

Pred (S : -Type) := S ->? Unit ;

Set (S : Type) := S ->? Unit ;

ops True, False : Bool;

ops emptySet : Set S;

{__} : S -> Set S;

__isIn__ : S * Set S ->? Unit;

__subset__ : Pred ( Set (S) * Set (S) );

__union__, __intersection__, __ \\ __ : Set S * Set S -> Set S;

__disjoint__ : Pred ( Set (S) * Set (S) );

__ * __ : Set S * Set T -> Set (S * T);

__disjointUnion__ : Set S * Set S -> Set (S * Bool);

inl, inr : S -> S * Bool;

forall x, x' : S; y : T; s, s' : Set (S); t : Set (T)

. not (x isIn emptySet)

. (x isIn {x'}) <=> x = x'

. (x isIn s) <=> (s x)

. (s subset s') <=> (forall x : S . x isIn s => x isIn s')

. x isIn (s union s') <=> x isIn s \/ x isIn s'

. x isIn (s intersection s') <=> x isIn s /\ x isIn s'

. x isIn (s \\ s') <=> x isIn s /\ not x isIn s'

. s disjoint s' <=> s intersection s' = emptySet

. (x, y) isIn (s * t) <=> x isIn s /\ y isIn t

. inl x = (x, False)

. inr x = (x, True)