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)